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