| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | brdom7disj.2 | . . 3
⊢ 𝐵 ∈ V | 
| 2 | 1 | brdom4 10570 | . 2
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) | 
| 3 |  | incom 4209 | . . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) | 
| 4 |  | brdom7disj.3 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ 𝐵) = ∅ | 
| 5 | 3, 4 | eqtri 2765 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 ∩ 𝐴) = ∅ | 
| 6 |  | disjne 4455 | . . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∩ 𝐴) = ∅ ∧ 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → 𝑥 ≠ 𝑤) | 
| 7 | 5, 6 | mp3an1 1450 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → 𝑥 ≠ 𝑤) | 
| 8 |  | vex 3484 | . . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V | 
| 9 |  | vex 3484 | . . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V | 
| 10 |  | vex 3484 | . . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V | 
| 11 |  | vex 3484 | . . . . . . . . . . . . . . . 16
⊢ 𝑤 ∈ V | 
| 12 | 8, 9, 10, 11 | opthpr 4851 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ≠ 𝑤 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) | 
| 13 | 7, 12 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) | 
| 14 |  | equcom 2017 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) | 
| 15 |  | equcom 2017 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 ↔ 𝑤 = 𝑦) | 
| 16 | 14, 15 | anbi12i 628 | . . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ↔ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) | 
| 17 | 13, 16 | bitr2di 288 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ↔ {𝑥, 𝑦} = {𝑧, 𝑤})) | 
| 18 |  | df-br 5144 | . . . . . . . . . . . . . 14
⊢ (𝑧𝑔𝑤 ↔ 〈𝑧, 𝑤〉 ∈ 𝑔) | 
| 19 | 18 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → (𝑧𝑔𝑤 ↔ 〈𝑧, 𝑤〉 ∈ 𝑔)) | 
| 20 | 17, 19 | anbi12d 632 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐴) → (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝑧𝑔𝑤) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) | 
| 21 | 20 | rexbidva 3177 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐵 → (∃𝑤 ∈ 𝐴 ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝑧𝑔𝑤) ↔ ∃𝑤 ∈ 𝐴 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) | 
| 22 | 21 | rexbidv 3179 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝑧𝑔𝑤) ↔ ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) | 
| 23 |  | rexcom 3290 | . . . . . . . . . . 11
⊢
(∃𝑧 ∈
𝐵 ∃𝑤 ∈ 𝐴 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)) | 
| 24 |  | zfpair2 5433 | . . . . . . . . . . . 12
⊢ {𝑥, 𝑦} ∈ V | 
| 25 |  | eqeq1 2741 | . . . . . . . . . . . . . 14
⊢ (𝑣 = {𝑥, 𝑦} → (𝑣 = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝑤})) | 
| 26 | 25 | anbi1d 631 | . . . . . . . . . . . . 13
⊢ (𝑣 = {𝑥, 𝑦} → ((𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) | 
| 27 | 26 | 2rexbidv 3222 | . . . . . . . . . . . 12
⊢ (𝑣 = {𝑥, 𝑦} → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) | 
| 28 | 24, 27 | elab 3679 | . . . . . . . . . . 11
⊢ ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)) | 
| 29 | 23, 28 | bitr4i 278 | . . . . . . . . . 10
⊢
(∃𝑧 ∈
𝐵 ∃𝑤 ∈ 𝐴 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)}) | 
| 30 | 22, 29 | bitr2di 288 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝑧𝑔𝑤))) | 
| 31 | 30 | adantr 480 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) → ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝑧𝑔𝑤))) | 
| 32 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝑧𝑔𝑤 ↔ 𝑥𝑔𝑤)) | 
| 33 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑥𝑔𝑤 ↔ 𝑥𝑔𝑦)) | 
| 34 | 32, 33 | ceqsrex2v 3658 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝑧𝑔𝑤) ↔ 𝑥𝑔𝑦)) | 
| 35 | 31, 34 | bitrd 279 | . . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) → ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ 𝑥𝑔𝑦)) | 
| 36 | 35 | rmobidva 3395 | . . . . . 6
⊢ (𝑥 ∈ 𝐵 → (∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦)) | 
| 37 | 36 | ralbiia 3091 | . . . . 5
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦) | 
| 38 |  | zfpair2 5433 | . . . . . . . . . . 11
⊢ {𝑦, 𝑥} ∈ V | 
| 39 |  | eqeq1 2741 | . . . . . . . . . . . . 13
⊢ (𝑣 = {𝑦, 𝑥} → (𝑣 = {𝑧, 𝑤} ↔ {𝑦, 𝑥} = {𝑧, 𝑤})) | 
| 40 | 39 | anbi1d 631 | . . . . . . . . . . . 12
⊢ (𝑣 = {𝑦, 𝑥} → ((𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) | 
| 41 | 40 | 2rexbidv 3222 | . . . . . . . . . . 11
⊢ (𝑣 = {𝑦, 𝑥} → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔))) | 
| 42 | 38, 41 | elab 3679 | . . . . . . . . . 10
⊢ ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)) | 
| 43 |  | disjne 4455 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∩ 𝐴) = ∅ ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑧 ≠ 𝑥) | 
| 44 | 5, 43 | mp3an1 1450 | . . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑧 ≠ 𝑥) | 
| 45 | 44 | ancoms 458 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝑧 ≠ 𝑥) | 
| 46 | 10, 11, 9, 8 | opthpr 4851 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ≠ 𝑥 → ({𝑧, 𝑤} = {𝑦, 𝑥} ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥))) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ({𝑧, 𝑤} = {𝑦, 𝑥} ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥))) | 
| 48 |  | eqcom 2744 | . . . . . . . . . . . . . 14
⊢ ({𝑦, 𝑥} = {𝑧, 𝑤} ↔ {𝑧, 𝑤} = {𝑦, 𝑥}) | 
| 49 |  | ancom 460 | . . . . . . . . . . . . . 14
⊢ ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ↔ (𝑧 = 𝑦 ∧ 𝑤 = 𝑥)) | 
| 50 | 47, 48, 49 | 3bitr4g 314 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ({𝑦, 𝑥} = {𝑧, 𝑤} ↔ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦))) | 
| 51 | 18 | bicomi 224 | . . . . . . . . . . . . . 14
⊢
(〈𝑧, 𝑤〉 ∈ 𝑔 ↔ 𝑧𝑔𝑤) | 
| 52 | 51 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ 𝑔 ↔ 𝑧𝑔𝑤)) | 
| 53 | 50, 52 | anbi12d 632 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) | 
| 54 | 53 | rexbidva 3177 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (∃𝑧 ∈ 𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) | 
| 55 | 54 | rexbidv 3179 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) | 
| 56 | 42, 55 | bitrid 283 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) | 
| 57 | 56 | adantr 480 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤))) | 
| 58 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑧𝑔𝑤 ↔ 𝑧𝑔𝑥)) | 
| 59 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧𝑔𝑥 ↔ 𝑦𝑔𝑥)) | 
| 60 | 58, 59 | ceqsrex2v 3658 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 ((𝑤 = 𝑥 ∧ 𝑧 = 𝑦) ∧ 𝑧𝑔𝑤) ↔ 𝑦𝑔𝑥)) | 
| 61 | 57, 60 | bitrd 279 | . . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ 𝑦𝑔𝑥)) | 
| 62 | 61 | rexbidva 3177 | . . . . . 6
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) | 
| 63 | 62 | ralbiia 3091 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) | 
| 64 |  | brdom7disj.1 | . . . . . . 7
⊢ 𝐴 ∈ V | 
| 65 |  | snex 5436 | . . . . . . . 8
⊢ {{𝑧, 𝑤}} ∈ V | 
| 66 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔) → 𝑣 = {𝑧, 𝑤}) | 
| 67 | 66 | ss2abi 4067 | . . . . . . . . 9
⊢ {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ⊆ {𝑣 ∣ 𝑣 = {𝑧, 𝑤}} | 
| 68 |  | df-sn 4627 | . . . . . . . . 9
⊢ {{𝑧, 𝑤}} = {𝑣 ∣ 𝑣 = {𝑧, 𝑤}} | 
| 69 | 67, 68 | sseqtrri 4033 | . . . . . . . 8
⊢ {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ⊆ {{𝑧, 𝑤}} | 
| 70 | 65, 69 | ssexi 5322 | . . . . . . 7
⊢ {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ∈ V | 
| 71 | 64, 1, 70 | ab2rexex2 8005 | . . . . . 6
⊢ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ∈ V | 
| 72 |  | eleq2 2830 | . . . . . . . . 9
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → ({𝑥, 𝑦} ∈ 𝑓 ↔ {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) | 
| 73 | 72 | rmobidv 3397 | . . . . . . . 8
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → (∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ↔ ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) | 
| 74 | 73 | ralbidv 3178 | . . . . . . 7
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) | 
| 75 |  | eleq2 2830 | . . . . . . . . 9
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → ({𝑦, 𝑥} ∈ 𝑓 ↔ {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) | 
| 76 | 75 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → (∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓 ↔ ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) | 
| 77 | 76 | ralbidv 3178 | . . . . . . 7
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)})) | 
| 78 | 74, 77 | anbi12d 632 | . . . . . 6
⊢ (𝑓 = {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} → ((∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) ↔ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)}))) | 
| 79 | 71, 78 | spcev 3606 | . . . . 5
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)} ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤 ∈ 𝐴 ∃𝑧 ∈ 𝐵 (𝑣 = {𝑧, 𝑤} ∧ 〈𝑧, 𝑤〉 ∈ 𝑔)}) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) | 
| 80 | 37, 63, 79 | syl2anbr 599 | . . . 4
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) | 
| 81 | 80 | exlimiv 1930 | . . 3
⊢
(∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) | 
| 82 |  | preq1 4733 | . . . . . . . . 9
⊢ (𝑤 = 𝑥 → {𝑤, 𝑧} = {𝑥, 𝑧}) | 
| 83 | 82 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑤 = 𝑥 → ({𝑤, 𝑧} ∈ 𝑓 ↔ {𝑥, 𝑧} ∈ 𝑓)) | 
| 84 |  | preq2 4734 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → {𝑥, 𝑧} = {𝑥, 𝑦}) | 
| 85 | 84 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → ({𝑥, 𝑧} ∈ 𝑓 ↔ {𝑥, 𝑦} ∈ 𝑓)) | 
| 86 |  | eqid 2737 | . . . . . . . 8
⊢
{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} | 
| 87 | 8, 9, 83, 85, 86 | brab 5548 | . . . . . . 7
⊢ (𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ {𝑥, 𝑦} ∈ 𝑓) | 
| 88 | 87 | rmobii 3388 | . . . . . 6
⊢
(∃*𝑦 ∈
𝐴 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓) | 
| 89 | 88 | ralbii 3093 | . . . . 5
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓) | 
| 90 |  | preq1 4733 | . . . . . . . . 9
⊢ (𝑤 = 𝑦 → {𝑤, 𝑧} = {𝑦, 𝑧}) | 
| 91 | 90 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑤 = 𝑦 → ({𝑤, 𝑧} ∈ 𝑓 ↔ {𝑦, 𝑧} ∈ 𝑓)) | 
| 92 |  | preq2 4734 | . . . . . . . . 9
⊢ (𝑧 = 𝑥 → {𝑦, 𝑧} = {𝑦, 𝑥}) | 
| 93 | 92 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑧 = 𝑥 → ({𝑦, 𝑧} ∈ 𝑓 ↔ {𝑦, 𝑥} ∈ 𝑓)) | 
| 94 | 9, 8, 91, 93, 86 | brab 5548 | . . . . . . 7
⊢ (𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ {𝑦, 𝑥} ∈ 𝑓) | 
| 95 | 94 | rexbii 3094 | . . . . . 6
⊢
(∃𝑦 ∈
𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) | 
| 96 | 95 | ralbii 3093 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) | 
| 97 |  | df-opab 5206 | . . . . . . 7
⊢
{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} = {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} | 
| 98 |  | vuniex 7759 | . . . . . . . 8
⊢ ∪ 𝑓
∈ V | 
| 99 | 11 | prid1 4762 | . . . . . . . . . . 11
⊢ 𝑤 ∈ {𝑤, 𝑧} | 
| 100 |  | elunii 4912 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ {𝑤, 𝑧} ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 ∈ ∪ 𝑓) | 
| 101 | 99, 100 | mpan 690 | . . . . . . . . . 10
⊢ ({𝑤, 𝑧} ∈ 𝑓 → 𝑤 ∈ ∪ 𝑓) | 
| 102 | 101 | adantl 481 | . . . . . . . . 9
⊢ ((𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 ∈ ∪ 𝑓) | 
| 103 | 102 | exlimiv 1930 | . . . . . . . 8
⊢
(∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 ∈ ∪ 𝑓) | 
| 104 | 10 | prid2 4763 | . . . . . . . . . . 11
⊢ 𝑧 ∈ {𝑤, 𝑧} | 
| 105 |  | elunii 4912 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ {𝑤, 𝑧} ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑧 ∈ ∪ 𝑓) | 
| 106 | 104, 105 | mpan 690 | . . . . . . . . . 10
⊢ ({𝑤, 𝑧} ∈ 𝑓 → 𝑧 ∈ ∪ 𝑓) | 
| 107 | 106 | adantl 481 | . . . . . . . . 9
⊢ ((𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑧 ∈ ∪ 𝑓) | 
| 108 |  | df-sn 4627 | . . . . . . . . . . 11
⊢
{〈𝑤, 𝑧〉} = {𝑣 ∣ 𝑣 = 〈𝑤, 𝑧〉} | 
| 109 |  | snex 5436 | . . . . . . . . . . 11
⊢
{〈𝑤, 𝑧〉} ∈
V | 
| 110 | 108, 109 | eqeltrri 2838 | . . . . . . . . . 10
⊢ {𝑣 ∣ 𝑣 = 〈𝑤, 𝑧〉} ∈ V | 
| 111 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑣 = 〈𝑤, 𝑧〉) | 
| 112 | 111 | ss2abi 4067 | . . . . . . . . . 10
⊢ {𝑣 ∣ (𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} ⊆ {𝑣 ∣ 𝑣 = 〈𝑤, 𝑧〉} | 
| 113 | 110, 112 | ssexi 5322 | . . . . . . . . 9
⊢ {𝑣 ∣ (𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V | 
| 114 | 98, 107, 113 | abexex 7996 | . . . . . . . 8
⊢ {𝑣 ∣ ∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V | 
| 115 | 98, 103, 114 | abexex 7996 | . . . . . . 7
⊢ {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V | 
| 116 | 97, 115 | eqeltri 2837 | . . . . . 6
⊢
{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} ∈ V | 
| 117 |  | breq 5145 | . . . . . . . . 9
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (𝑥𝑔𝑦 ↔ 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦)) | 
| 118 | 117 | rmobidv 3397 | . . . . . . . 8
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ↔ ∃*𝑦 ∈ 𝐴 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦)) | 
| 119 | 118 | ralbidv 3178 | . . . . . . 7
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ↔ ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦)) | 
| 120 |  | breq 5145 | . . . . . . . . 9
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (𝑦𝑔𝑥 ↔ 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥)) | 
| 121 | 120 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (∃𝑦 ∈ 𝐵 𝑦𝑔𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥)) | 
| 122 | 121 | ralbidv 3178 | . . . . . . 7
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥)) | 
| 123 | 119, 122 | anbi12d 632 | . . . . . 6
⊢ (𝑔 = {〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓} → ((∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) ↔ (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥))) | 
| 124 | 116, 123 | spcev 3606 | . . . . 5
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦{〈𝑤, 𝑧〉 ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥) → ∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) | 
| 125 | 89, 96, 124 | syl2anbr 599 | . . . 4
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) → ∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) | 
| 126 | 125 | exlimiv 1930 | . . 3
⊢
(∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓) → ∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥)) | 
| 127 | 81, 126 | impbii 209 | . 2
⊢
(∃𝑔(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑔𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑔𝑥) ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) | 
| 128 | 2, 127 | bitri 275 | 1
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 {𝑦, 𝑥} ∈ 𝑓)) |