MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brdom6disj Structured version   Visualization version   GIF version

Theorem brdom6disj 10523
Description: An equivalence to a dominance relation for disjoint sets. (Contributed by NM, 5-Apr-2007.)
Hypotheses
Ref Expression
brdom7disj.1 𝐴 ∈ V
brdom7disj.2 𝐵 ∈ V
brdom7disj.3 (𝐴𝐵) = ∅
Assertion
Ref Expression
brdom6disj (𝐴𝐵 ↔ ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
Distinct variable groups:   𝑥,𝑓,𝑦,𝐴   𝐵,𝑓,𝑥,𝑦

Proof of Theorem brdom6disj
Dummy variables 𝑔 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdom7disj.2 . . 3 𝐵 ∈ V
21brdom5 10520 . 2 (𝐴𝐵 ↔ ∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥))
3 zfpair2 5418 . . . . . . . . 9 {𝑥, 𝑦} ∈ V
4 eqeq1 2728 . . . . . . . . . . . 12 (𝑣 = {𝑥, 𝑦} → (𝑣 = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝑤}))
54anbi1d 629 . . . . . . . . . . 11 (𝑣 = {𝑥, 𝑦} → ((𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)))
6 df-br 5139 . . . . . . . . . . . 12 (𝑧𝑔𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑔)
76anbi2i 622 . . . . . . . . . . 11 (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔))
85, 7bitr4di 289 . . . . . . . . . 10 (𝑣 = {𝑥, 𝑦} → ((𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤)))
982rexbidv 3211 . . . . . . . . 9 (𝑣 = {𝑥, 𝑦} → (∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ∃𝑤𝐴𝑧𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤)))
103, 9elab 3660 . . . . . . . 8 ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑤𝐴𝑧𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤))
11 incom 4193 . . . . . . . . . . . . . . . 16 (𝐵𝐴) = (𝐴𝐵)
12 brdom7disj.3 . . . . . . . . . . . . . . . 16 (𝐴𝐵) = ∅
1311, 12eqtri 2752 . . . . . . . . . . . . . . 15 (𝐵𝐴) = ∅
14 disjne 4446 . . . . . . . . . . . . . . 15 (((𝐵𝐴) = ∅ ∧ 𝑥𝐵𝑤𝐴) → 𝑥𝑤)
1513, 14mp3an1 1444 . . . . . . . . . . . . . 14 ((𝑥𝐵𝑤𝐴) → 𝑥𝑤)
16 vex 3470 . . . . . . . . . . . . . . 15 𝑥 ∈ V
17 vex 3470 . . . . . . . . . . . . . . 15 𝑦 ∈ V
18 vex 3470 . . . . . . . . . . . . . . 15 𝑧 ∈ V
19 vex 3470 . . . . . . . . . . . . . . 15 𝑤 ∈ V
2016, 17, 18, 19opthpr 4844 . . . . . . . . . . . . . 14 (𝑥𝑤 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 = 𝑧𝑦 = 𝑤)))
2115, 20syl 17 . . . . . . . . . . . . 13 ((𝑥𝐵𝑤𝐴) → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 = 𝑧𝑦 = 𝑤)))
22 breq12 5143 . . . . . . . . . . . . . 14 ((𝑥 = 𝑧𝑦 = 𝑤) → (𝑥𝑔𝑦𝑧𝑔𝑤))
2322biimprd 247 . . . . . . . . . . . . 13 ((𝑥 = 𝑧𝑦 = 𝑤) → (𝑧𝑔𝑤𝑥𝑔𝑦))
2421, 23biimtrdi 252 . . . . . . . . . . . 12 ((𝑥𝐵𝑤𝐴) → ({𝑥, 𝑦} = {𝑧, 𝑤} → (𝑧𝑔𝑤𝑥𝑔𝑦)))
2524impd 410 . . . . . . . . . . 11 ((𝑥𝐵𝑤𝐴) → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦))
2625ex 412 . . . . . . . . . 10 (𝑥𝐵 → (𝑤𝐴 → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦)))
2726adantrd 491 . . . . . . . . 9 (𝑥𝐵 → ((𝑤𝐴𝑧𝐵) → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦)))
2827rexlimdvv 3202 . . . . . . . 8 (𝑥𝐵 → (∃𝑤𝐴𝑧𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦))
2910, 28biimtrid 241 . . . . . . 7 (𝑥𝐵 → ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → 𝑥𝑔𝑦))
3029moimdv 2532 . . . . . 6 (𝑥𝐵 → (∃*𝑦 𝑥𝑔𝑦 → ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
3130ralimia 3072 . . . . 5 (∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 → ∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)})
32 zfpair2 5418 . . . . . . . . . . . 12 {𝑦, 𝑥} ∈ V
33 eqeq1 2728 . . . . . . . . . . . . . 14 (𝑣 = {𝑦, 𝑥} → (𝑣 = {𝑧, 𝑤} ↔ {𝑦, 𝑥} = {𝑧, 𝑤}))
3433anbi1d 629 . . . . . . . . . . . . 13 (𝑣 = {𝑦, 𝑥} → ((𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)))
35342rexbidv 3211 . . . . . . . . . . . 12 (𝑣 = {𝑦, 𝑥} → (∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ∃𝑤𝐴𝑧𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)))
3632, 35elab 3660 . . . . . . . . . . 11 ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑤𝐴𝑧𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔))
37 disjne 4446 . . . . . . . . . . . . . . . . . 18 (((𝐵𝐴) = ∅ ∧ 𝑧𝐵𝑥𝐴) → 𝑧𝑥)
3813, 37mp3an1 1444 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑥𝐴) → 𝑧𝑥)
3938ancoms 458 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑧𝐵) → 𝑧𝑥)
4018, 19, 17, 16opthpr 4844 . . . . . . . . . . . . . . . 16 (𝑧𝑥 → ({𝑧, 𝑤} = {𝑦, 𝑥} ↔ (𝑧 = 𝑦𝑤 = 𝑥)))
4139, 40syl 17 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑧𝐵) → ({𝑧, 𝑤} = {𝑦, 𝑥} ↔ (𝑧 = 𝑦𝑤 = 𝑥)))
42 eqcom 2731 . . . . . . . . . . . . . . 15 ({𝑦, 𝑥} = {𝑧, 𝑤} ↔ {𝑧, 𝑤} = {𝑦, 𝑥})
43 ancom 460 . . . . . . . . . . . . . . 15 ((𝑤 = 𝑥𝑧 = 𝑦) ↔ (𝑧 = 𝑦𝑤 = 𝑥))
4441, 42, 433bitr4g 314 . . . . . . . . . . . . . 14 ((𝑥𝐴𝑧𝐵) → ({𝑦, 𝑥} = {𝑧, 𝑤} ↔ (𝑤 = 𝑥𝑧 = 𝑦)))
456bicomi 223 . . . . . . . . . . . . . . 15 (⟨𝑧, 𝑤⟩ ∈ 𝑔𝑧𝑔𝑤)
4645a1i 11 . . . . . . . . . . . . . 14 ((𝑥𝐴𝑧𝐵) → (⟨𝑧, 𝑤⟩ ∈ 𝑔𝑧𝑔𝑤))
4744, 46anbi12d 630 . . . . . . . . . . . . 13 ((𝑥𝐴𝑧𝐵) → (({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
4847rexbidva 3168 . . . . . . . . . . . 12 (𝑥𝐴 → (∃𝑧𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ∃𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
4948rexbidv 3170 . . . . . . . . . . 11 (𝑥𝐴 → (∃𝑤𝐴𝑧𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ∃𝑤𝐴𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
5036, 49bitrid 283 . . . . . . . . . 10 (𝑥𝐴 → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑤𝐴𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
5150adantr 480 . . . . . . . . 9 ((𝑥𝐴𝑦𝐵) → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑤𝐴𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
52 breq2 5142 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑧𝑔𝑤𝑧𝑔𝑥))
53 breq1 5141 . . . . . . . . . 10 (𝑧 = 𝑦 → (𝑧𝑔𝑥𝑦𝑔𝑥))
5452, 53ceqsrex2v 3638 . . . . . . . . 9 ((𝑥𝐴𝑦𝐵) → (∃𝑤𝐴𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤) ↔ 𝑦𝑔𝑥))
5551, 54bitrd 279 . . . . . . . 8 ((𝑥𝐴𝑦𝐵) → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ 𝑦𝑔𝑥))
5655rexbidva 3168 . . . . . . 7 (𝑥𝐴 → (∃𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑦𝐵 𝑦𝑔𝑥))
5756ralbiia 3083 . . . . . 6 (∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥)
5857biimpri 227 . . . . 5 (∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥 → ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)})
59 brdom7disj.1 . . . . . . 7 𝐴 ∈ V
60 snex 5421 . . . . . . . 8 {{𝑧, 𝑤}} ∈ V
61 simpl 482 . . . . . . . . . 10 ((𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) → 𝑣 = {𝑧, 𝑤})
6261ss2abi 4055 . . . . . . . . 9 {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ⊆ {𝑣𝑣 = {𝑧, 𝑤}}
63 df-sn 4621 . . . . . . . . 9 {{𝑧, 𝑤}} = {𝑣𝑣 = {𝑧, 𝑤}}
6462, 63sseqtrri 4011 . . . . . . . 8 {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ⊆ {{𝑧, 𝑤}}
6560, 64ssexi 5312 . . . . . . 7 {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ∈ V
6659, 1, 65ab2rexex2 7960 . . . . . 6 {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ∈ V
67 eleq2 2814 . . . . . . . . 9 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → ({𝑥, 𝑦} ∈ 𝑓 ↔ {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
6867mobidv 2535 . . . . . . . 8 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → (∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ↔ ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
6968ralbidv 3169 . . . . . . 7 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → (∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ↔ ∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
70 eleq2 2814 . . . . . . . . 9 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → ({𝑦, 𝑥} ∈ 𝑓 ↔ {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
7170rexbidv 3170 . . . . . . . 8 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → (∃𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓 ↔ ∃𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
7271ralbidv 3169 . . . . . . 7 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → (∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓 ↔ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
7369, 72anbi12d 630 . . . . . 6 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → ((∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓) ↔ (∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)})))
7466, 73spcev 3588 . . . . 5 ((∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}) → ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
7531, 58, 74syl2an 595 . . . 4 ((∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥) → ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
7675exlimiv 1925 . . 3 (∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥) → ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
77 preq1 4729 . . . . . . . . 9 (𝑤 = 𝑥 → {𝑤, 𝑧} = {𝑥, 𝑧})
7877eleq1d 2810 . . . . . . . 8 (𝑤 = 𝑥 → ({𝑤, 𝑧} ∈ 𝑓 ↔ {𝑥, 𝑧} ∈ 𝑓))
79 preq2 4730 . . . . . . . . 9 (𝑧 = 𝑦 → {𝑥, 𝑧} = {𝑥, 𝑦})
8079eleq1d 2810 . . . . . . . 8 (𝑧 = 𝑦 → ({𝑥, 𝑧} ∈ 𝑓 ↔ {𝑥, 𝑦} ∈ 𝑓))
81 eqid 2724 . . . . . . . 8 {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}
8216, 17, 78, 80, 81brab 5533 . . . . . . 7 (𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ {𝑥, 𝑦} ∈ 𝑓)
8382mobii 2534 . . . . . 6 (∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ ∃*𝑦{𝑥, 𝑦} ∈ 𝑓)
8483ralbii 3085 . . . . 5 (∀𝑥𝐵 ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ ∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓)
85 preq1 4729 . . . . . . . . 9 (𝑤 = 𝑦 → {𝑤, 𝑧} = {𝑦, 𝑧})
8685eleq1d 2810 . . . . . . . 8 (𝑤 = 𝑦 → ({𝑤, 𝑧} ∈ 𝑓 ↔ {𝑦, 𝑧} ∈ 𝑓))
87 preq2 4730 . . . . . . . . 9 (𝑧 = 𝑥 → {𝑦, 𝑧} = {𝑦, 𝑥})
8887eleq1d 2810 . . . . . . . 8 (𝑧 = 𝑥 → ({𝑦, 𝑧} ∈ 𝑓 ↔ {𝑦, 𝑥} ∈ 𝑓))
8917, 16, 86, 88, 81brab 5533 . . . . . . 7 (𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ {𝑦, 𝑥} ∈ 𝑓)
9089rexbii 3086 . . . . . 6 (∃𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ ∃𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓)
9190ralbii 3085 . . . . 5 (∀𝑥𝐴𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓)
92 df-opab 5201 . . . . . . 7 {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} = {𝑣 ∣ ∃𝑤𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)}
93 vuniex 7722 . . . . . . . 8 𝑓 ∈ V
9419prid1 4758 . . . . . . . . . . 11 𝑤 ∈ {𝑤, 𝑧}
95 elunii 4904 . . . . . . . . . . 11 ((𝑤 ∈ {𝑤, 𝑧} ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 𝑓)
9694, 95mpan 687 . . . . . . . . . 10 ({𝑤, 𝑧} ∈ 𝑓𝑤 𝑓)
9796adantl 481 . . . . . . . . 9 ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 𝑓)
9897exlimiv 1925 . . . . . . . 8 (∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 𝑓)
9918prid2 4759 . . . . . . . . . . 11 𝑧 ∈ {𝑤, 𝑧}
100 elunii 4904 . . . . . . . . . . 11 ((𝑧 ∈ {𝑤, 𝑧} ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑧 𝑓)
10199, 100mpan 687 . . . . . . . . . 10 ({𝑤, 𝑧} ∈ 𝑓𝑧 𝑓)
102101adantl 481 . . . . . . . . 9 ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑧 𝑓)
103 df-sn 4621 . . . . . . . . . . 11 {⟨𝑤, 𝑧⟩} = {𝑣𝑣 = ⟨𝑤, 𝑧⟩}
104 snex 5421 . . . . . . . . . . 11 {⟨𝑤, 𝑧⟩} ∈ V
105103, 104eqeltrri 2822 . . . . . . . . . 10 {𝑣𝑣 = ⟨𝑤, 𝑧⟩} ∈ V
106 simpl 482 . . . . . . . . . . 11 ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑣 = ⟨𝑤, 𝑧⟩)
107106ss2abi 4055 . . . . . . . . . 10 {𝑣 ∣ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)} ⊆ {𝑣𝑣 = ⟨𝑤, 𝑧⟩}
108105, 107ssexi 5312 . . . . . . . . 9 {𝑣 ∣ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V
10993, 102, 108abexex 7951 . . . . . . . 8 {𝑣 ∣ ∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V
11093, 98, 109abexex 7951 . . . . . . 7 {𝑣 ∣ ∃𝑤𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V
11192, 110eqeltri 2821 . . . . . 6 {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} ∈ V
112 breq 5140 . . . . . . . . 9 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (𝑥𝑔𝑦𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦))
113112mobidv 2535 . . . . . . . 8 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (∃*𝑦 𝑥𝑔𝑦 ↔ ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦))
114113ralbidv 3169 . . . . . . 7 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ↔ ∀𝑥𝐵 ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦))
115 breq 5140 . . . . . . . . 9 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (𝑦𝑔𝑥𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥))
116115rexbidv 3170 . . . . . . . 8 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (∃𝑦𝐵 𝑦𝑔𝑥 ↔ ∃𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥))
117116ralbidv 3169 . . . . . . 7 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥 ↔ ∀𝑥𝐴𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥))
118114, 117anbi12d 630 . . . . . 6 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → ((∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥) ↔ (∀𝑥𝐵 ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥)))
119111, 118spcev 3588 . . . . 5 ((∀𝑥𝐵 ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥) → ∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥))
12084, 91, 119syl2anbr 598 . . . 4 ((∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓) → ∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥))
121120exlimiv 1925 . . 3 (∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓) → ∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥))
12276, 121impbii 208 . 2 (∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥) ↔ ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
1232, 122bitri 275 1 (𝐴𝐵 ↔ ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1533  wex 1773  wcel 2098  ∃*wmo 2524  {cab 2701  wne 2932  wral 3053  wrex 3062  Vcvv 3466  cin 3939  c0 4314  {csn 4620  {cpr 4622  cop 4626   cuni 4899   class class class wbr 5138  {copab 5200  cdom 8933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-ac2 10454
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-card 9930  df-acn 9933  df-ac 10107
This theorem is referenced by:  grothprim  10825
  Copyright terms: Public domain W3C validator