Step | Hyp | Ref
| Expression |
1 | | brdom7disj.2 |
. . 3
⊢ 𝐵 ∈ V |
2 | 1 | brdom5 9232 |
. 2
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) |
3 | | zfpair2 4834 |
. . . . . . . . . 10
⊢ {𝑥, 𝑦} ∈ V |
4 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝑣 = {𝑥, 𝑦} → (𝑣 = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝑤})) |
5 | 4 | anbi1d 737 |
. . . . . . . . . . . 12
⊢ (𝑣 = {𝑥, 𝑦} → ((𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) |
6 | | df-br 4584 |
. . . . . . . . . . . . 13
⊢ (𝑧𝑔𝑤 ↔ 〈𝑧, 𝑤〉 ∈ 𝑔) |
7 | 6 | anbi2i 726 |
. . . . . . . . . . . 12
⊢ (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)) |
8 | 5, 7 | syl6bbr 277 |
. . . . . . . . . . 11
⊢ (𝑣 = {𝑥, 𝑦} → ((𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤))) |
9 | 8 | 2rexbidv 3039 |
. . . . . . . . . 10
⊢ (𝑣 = {𝑥, 𝑦} → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤))) |
10 | 3, 9 | elab 3319 |
. . . . . . . . 9
⊢ ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤)) |
11 | | incom 3767 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) |
12 | | brdom7disj.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ 𝐵) = ∅ |
13 | 11, 12 | eqtri 2632 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∩ 𝐴) = ∅ |
14 | | disjne 3974 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∩ 𝐴) = ∅ ∧ 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → 𝑥 ≠ 𝑤) |
15 | 13, 14 | mp3an1 1403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → 𝑥 ≠ 𝑤) |
16 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
17 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
18 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
19 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑤 ∈ V |
20 | 16, 17, 18, 19 | opthpr 4324 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ≠ 𝑤 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
21 | 15, 20 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
22 | | breq12 4588 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥𝑔𝑦 ↔ 𝑧𝑔𝑤)) |
23 | 22 | biimprd 237 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑧𝑔𝑤 → 𝑥𝑔𝑦)) |
24 | 21, 23 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → ({𝑥, 𝑦} = {𝑧, 𝑤} → (𝑧𝑔𝑤 → 𝑥𝑔𝑦))) |
25 | 24 | impd 446 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦)) |
26 | 25 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐵 → (𝑤 ∈ 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦))) |
27 | 26 | adantrd 483 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → ((𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦))) |
28 | 27 | rexlimdvv 3019 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦)) |
29 | 10, 28 | syl5bi 231 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → 𝑥𝑔𝑦)) |
30 | 29 | alrimiv 1842 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → ∀𝑦({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → 𝑥𝑔𝑦)) |
31 | | moim 2507 |
. . . . . . 7
⊢
(∀𝑦({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → 𝑥𝑔𝑦) → (∃*𝑦 𝑥𝑔𝑦 → ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 → (∃*𝑦 𝑥𝑔𝑦 → ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) |
33 | 32 | ralimia 2934 |
. . . . 5
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑔𝑦 → ∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)}) |
34 | | zfpair2 4834 |
. . . . . . . . . . . 12
⊢ {𝑦, 𝑥} ∈ V |
35 | | eqeq1 2614 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = {𝑦, 𝑥} → (𝑣 = {𝑧, 𝑤} ↔ {𝑦, 𝑥} = {𝑧, 𝑤})) |
36 | 35 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑣 = {𝑦, 𝑥} → ((𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) |
37 | 36 | 2rexbidv 3039 |
. . . . . . . . . . . 12
⊢ (𝑣 = {𝑦, 𝑥} → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) |
38 | 34, 37 | elab 3319 |
. . . . . . . . . . 11
⊢ ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)) |
39 | | disjne 3974 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∩ 𝐴) = ∅ ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑧 ≠ 𝑥) |
40 | 13, 39 | mp3an1 1403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑧 ≠ 𝑥) |
41 | 40 | ancoms 468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝑧 ≠ 𝑥) |
42 | 18, 19, 17, 16 | opthpr 4324 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ≠ 𝑥 → ({𝑧, 𝑤} = {𝑦, 𝑥} ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ({𝑧, 𝑤} = {𝑦, 𝑥} ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥))) |
44 | | eqcom 2617 |
. . . . . . . . . . . . . . 15
⊢ ({𝑦, 𝑥} = {𝑧, 𝑤} ↔ {𝑧, 𝑤} = {𝑦, 𝑥}) |
45 | | ancom 465 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥)) |
46 | 43, 44, 45 | 3bitr4g 302 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ({𝑦, 𝑥} = {𝑧, 𝑤} ↔ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦))) |
47 | 6 | bicomi 213 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑧, 𝑤〉 ∈ 𝑔 ↔ 𝑧𝑔𝑤) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ 𝑔 ↔ 𝑧𝑔𝑤)) |
49 | 46, 48 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) |
50 | 49 | rexbidva 3031 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → (∃𝑧 ∈ 𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) |
51 | 50 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) |
52 | 38, 51 | syl5bb 271 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) |
53 | 52 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) |
54 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑧𝑔𝑤 ↔ 𝑧𝑔𝑥)) |
55 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑧𝑔𝑥 ↔ 𝑦𝑔𝑥)) |
56 | 54, 55 | ceqsrex2v 3308 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤) ↔ 𝑦𝑔𝑥)) |
57 | 53, 56 | bitrd 267 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ 𝑦𝑔𝑥)) |
58 | 57 | rexbidva 3031 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) |
59 | 58 | ralbiia 2962 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) |
60 | 59 | biimpri 217 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)}) |
61 | | brdom7disj.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
62 | | snex 4835 |
. . . . . . . 8
⊢ {{𝑧, 𝑤}} ∈ V |
63 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) → 𝑣 = {𝑧, 𝑤}) |
64 | 63 | ss2abi 3637 |
. . . . . . . . 9
⊢ {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ⊆ {𝑣 ∣ 𝑣 = {𝑧, 𝑤}} |
65 | | df-sn 4126 |
. . . . . . . . 9
⊢ {{𝑧, 𝑤}} = {𝑣 ∣ 𝑣 = {𝑧, 𝑤}} |
66 | 64, 65 | sseqtr4i 3601 |
. . . . . . . 8
⊢ {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ⊆ {{𝑧, 𝑤}} |
67 | 62, 66 | ssexi 4731 |
. . . . . . 7
⊢ {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ∈ V |
68 | 61, 1, 67 | ab2rexex2 7051 |
. . . . . 6
⊢ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ∈ V |
69 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → ({𝑥, 𝑦} ∈ 𝑓 ↔ {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) |
70 | 69 | mobidv 2479 |
. . . . . . . 8
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → (∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ↔ ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) |
71 | 70 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → (∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) |
72 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → ({𝑦, 𝑥} ∈ 𝑓 ↔ {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) |
73 | 72 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → (∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓 ↔ ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) |
74 | 73 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) |
75 | 71, 74 | anbi12d 743 |
. . . . . 6
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → ((∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) ↔ (∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)}))) |
76 | 68, 75 | spcev 3273 |
. . . . 5
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)}) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) |
77 | 33, 60, 76 | syl2an 493 |
. . . 4
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) |
78 | 77 | exlimiv 1845 |
. . 3
⊢
(∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) |
79 | | preq1 4212 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → {𝑤, 𝑧} = {𝑥, 𝑧}) |
80 | 79 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ({𝑤, 𝑧} ∈ 𝑓 ↔ {𝑥, 𝑧} ∈ 𝑓)) |
81 | | preq2 4213 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → {𝑥, 𝑧} = {𝑥, 𝑦}) |
82 | 81 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ({𝑥, 𝑧} ∈ 𝑓 ↔ {𝑥, 𝑦} ∈ 𝑓)) |
83 | | eqid 2610 |
. . . . . . . 8
⊢
{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} |
84 | 16, 17, 80, 82, 83 | brab 4923 |
. . . . . . 7
⊢ (𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ {𝑥, 𝑦} ∈ 𝑓) |
85 | 84 | mobii 2481 |
. . . . . 6
⊢
(∃*𝑦 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ ∃*𝑦{𝑥, 𝑦} ∈ 𝑓) |
86 | 85 | ralbii 2963 |
. . . . 5
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓) |
87 | | preq1 4212 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → {𝑤, 𝑧} = {𝑦, 𝑧}) |
88 | 87 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ({𝑤, 𝑧} ∈ 𝑓 ↔ {𝑦, 𝑧} ∈ 𝑓)) |
89 | | preq2 4213 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → {𝑦, 𝑧} = {𝑦, 𝑥}) |
90 | 89 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → ({𝑦, 𝑧} ∈ 𝑓 ↔ {𝑦, 𝑥} ∈ 𝑓)) |
91 | 17, 16, 88, 90, 83 | brab 4923 |
. . . . . . 7
⊢ (𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ {𝑦, 𝑥} ∈ 𝑓) |
92 | 91 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) |
93 | 92 | ralbii 2963 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) |
94 | | df-opab 4644 |
. . . . . . 7
⊢
{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} = {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} |
95 | | vuniex 6852 |
. . . . . . . 8
⊢ ∪ 𝑓
∈ V |
96 | 19 | prid1 4241 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ {𝑤, 𝑧} |
97 | | elunii 4377 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ {𝑤, 𝑧} ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 ∈ ∪ 𝑓) |
98 | 96, 97 | mpan 702 |
. . . . . . . . . 10
⊢ ({𝑤, 𝑧} ∈ 𝑓 → 𝑤 ∈ ∪ 𝑓) |
99 | 98 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 ∈ ∪ 𝑓) |
100 | 99 | exlimiv 1845 |
. . . . . . . 8
⊢
(∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 ∈ ∪ 𝑓) |
101 | 18 | prid2 4242 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ {𝑤, 𝑧} |
102 | | elunii 4377 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ {𝑤, 𝑧} ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑧 ∈ ∪ 𝑓) |
103 | 101, 102 | mpan 702 |
. . . . . . . . . 10
⊢ ({𝑤, 𝑧} ∈ 𝑓 → 𝑧 ∈ ∪ 𝑓) |
104 | 103 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑧 ∈ ∪ 𝑓) |
105 | | df-sn 4126 |
. . . . . . . . . . 11
⊢
{〈𝑤, 𝑧〉} = {𝑣 ∣ 𝑣 = 〈𝑤, 𝑧〉} |
106 | | snex 4835 |
. . . . . . . . . . 11
⊢
{〈𝑤, 𝑧〉} ∈
V |
107 | 105, 106 | eqeltrri 2685 |
. . . . . . . . . 10
⊢ {𝑣 ∣ 𝑣 = 〈𝑤, 𝑧〉} ∈ V |
108 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑣 = 〈𝑤, 𝑧〉) |
109 | 108 | ss2abi 3637 |
. . . . . . . . . 10
⊢ {𝑣 ∣ (𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} ⊆ {𝑣 ∣ 𝑣 = 〈𝑤, 𝑧〉} |
110 | 107, 109 | ssexi 4731 |
. . . . . . . . 9
⊢ {𝑣 ∣ (𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V |
111 | 95, 104, 110 | abexex 7042 |
. . . . . . . 8
⊢ {𝑣 ∣ ∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V |
112 | 95, 100, 111 | abexex 7042 |
. . . . . . 7
⊢ {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V |
113 | 94, 112 | eqeltri 2684 |
. . . . . 6
⊢
{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} ∈ V |
114 | | breq 4585 |
. . . . . . . . 9
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (𝑥𝑔𝑦 ↔ 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦)) |
115 | 114 | mobidv 2479 |
. . . . . . . 8
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (∃*𝑦 𝑥𝑔𝑦 ↔ ∃*𝑦 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦)) |
116 | 115 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑔𝑦 ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦)) |
117 | | breq 4585 |
. . . . . . . . 9
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (𝑦𝑔𝑥 ↔ 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥)) |
118 | 117 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (∃𝑦 ∈ 𝐵 𝑦𝑔𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥)) |
119 | 118 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥)) |
120 | 116, 119 | anbi12d 743 |
. . . . . 6
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → ((∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) ↔ (∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥))) |
121 | 113, 120 | spcev 3273 |
. . . . 5
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥) → ∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) |
122 | 86, 93, 121 | syl2anbr 496 |
. . . 4
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) → ∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) |
123 | 122 | exlimiv 1845 |
. . 3
⊢
(∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) → ∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) |
124 | 78, 123 | impbii 198 |
. 2
⊢
(∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) |
125 | 2, 124 | bitri 263 |
1
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) |