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

Theorem brdom6disj 9298
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 9295 . 2 (𝐴𝐵 ↔ ∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥))
3 zfpair2 4868 . . . . . . . . . 10 {𝑥, 𝑦} ∈ V
4 eqeq1 2625 . . . . . . . . . . . . 13 (𝑣 = {𝑥, 𝑦} → (𝑣 = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝑤}))
54anbi1d 740 . . . . . . . . . . . 12 (𝑣 = {𝑥, 𝑦} → ((𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)))
6 df-br 4614 . . . . . . . . . . . . 13 (𝑧𝑔𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑔)
76anbi2i 729 . . . . . . . . . . . 12 (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔))
85, 7syl6bbr 278 . . . . . . . . . . 11 (𝑣 = {𝑥, 𝑦} → ((𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤)))
982rexbidv 3050 . . . . . . . . . 10 (𝑣 = {𝑥, 𝑦} → (∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ∃𝑤𝐴𝑧𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤)))
103, 9elab 3333 . . . . . . . . 9 ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑤𝐴𝑧𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤))
11 incom 3783 . . . . . . . . . . . . . . . . 17 (𝐵𝐴) = (𝐴𝐵)
12 brdom7disj.3 . . . . . . . . . . . . . . . . 17 (𝐴𝐵) = ∅
1311, 12eqtri 2643 . . . . . . . . . . . . . . . 16 (𝐵𝐴) = ∅
14 disjne 3994 . . . . . . . . . . . . . . . 16 (((𝐵𝐴) = ∅ ∧ 𝑥𝐵𝑤𝐴) → 𝑥𝑤)
1513, 14mp3an1 1408 . . . . . . . . . . . . . . 15 ((𝑥𝐵𝑤𝐴) → 𝑥𝑤)
16 vex 3189 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
17 vex 3189 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
18 vex 3189 . . . . . . . . . . . . . . . 16 𝑧 ∈ V
19 vex 3189 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
2016, 17, 18, 19opthpr 4352 . . . . . . . . . . . . . . 15 (𝑥𝑤 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 = 𝑧𝑦 = 𝑤)))
2115, 20syl 17 . . . . . . . . . . . . . 14 ((𝑥𝐵𝑤𝐴) → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ (𝑥 = 𝑧𝑦 = 𝑤)))
22 breq12 4618 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑧𝑦 = 𝑤) → (𝑥𝑔𝑦𝑧𝑔𝑤))
2322biimprd 238 . . . . . . . . . . . . . 14 ((𝑥 = 𝑧𝑦 = 𝑤) → (𝑧𝑔𝑤𝑥𝑔𝑦))
2421, 23syl6bi 243 . . . . . . . . . . . . 13 ((𝑥𝐵𝑤𝐴) → ({𝑥, 𝑦} = {𝑧, 𝑤} → (𝑧𝑔𝑤𝑥𝑔𝑦)))
2524impd 447 . . . . . . . . . . . 12 ((𝑥𝐵𝑤𝐴) → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦))
2625ex 450 . . . . . . . . . . 11 (𝑥𝐵 → (𝑤𝐴 → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦)))
2726adantrd 484 . . . . . . . . . 10 (𝑥𝐵 → ((𝑤𝐴𝑧𝐵) → (({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦)))
2827rexlimdvv 3030 . . . . . . . . 9 (𝑥𝐵 → (∃𝑤𝐴𝑧𝐵 ({𝑥, 𝑦} = {𝑧, 𝑤} ∧ 𝑧𝑔𝑤) → 𝑥𝑔𝑦))
2910, 28syl5bi 232 . . . . . . . 8 (𝑥𝐵 → ({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → 𝑥𝑔𝑦))
3029alrimiv 1852 . . . . . . 7 (𝑥𝐵 → ∀𝑦({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → 𝑥𝑔𝑦))
31 moim 2518 . . . . . . 7 (∀𝑦({𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → 𝑥𝑔𝑦) → (∃*𝑦 𝑥𝑔𝑦 → ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
3230, 31syl 17 . . . . . 6 (𝑥𝐵 → (∃*𝑦 𝑥𝑔𝑦 → ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
3332ralimia 2945 . . . . 5 (∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 → ∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)})
34 zfpair2 4868 . . . . . . . . . . . 12 {𝑦, 𝑥} ∈ V
35 eqeq1 2625 . . . . . . . . . . . . . 14 (𝑣 = {𝑦, 𝑥} → (𝑣 = {𝑧, 𝑤} ↔ {𝑦, 𝑥} = {𝑧, 𝑤}))
3635anbi1d 740 . . . . . . . . . . . . 13 (𝑣 = {𝑦, 𝑥} → ((𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)))
37362rexbidv 3050 . . . . . . . . . . . 12 (𝑣 = {𝑦, 𝑥} → (∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ∃𝑤𝐴𝑧𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)))
3834, 37elab 3333 . . . . . . . . . . 11 ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑤𝐴𝑧𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔))
39 disjne 3994 . . . . . . . . . . . . . . . . . 18 (((𝐵𝐴) = ∅ ∧ 𝑧𝐵𝑥𝐴) → 𝑧𝑥)
4013, 39mp3an1 1408 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑥𝐴) → 𝑧𝑥)
4140ancoms 469 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑧𝐵) → 𝑧𝑥)
4218, 19, 17, 16opthpr 4352 . . . . . . . . . . . . . . . 16 (𝑧𝑥 → ({𝑧, 𝑤} = {𝑦, 𝑥} ↔ (𝑧 = 𝑦𝑤 = 𝑥)))
4341, 42syl 17 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑧𝐵) → ({𝑧, 𝑤} = {𝑦, 𝑥} ↔ (𝑧 = 𝑦𝑤 = 𝑥)))
44 eqcom 2628 . . . . . . . . . . . . . . 15 ({𝑦, 𝑥} = {𝑧, 𝑤} ↔ {𝑧, 𝑤} = {𝑦, 𝑥})
45 ancom 466 . . . . . . . . . . . . . . 15 ((𝑤 = 𝑥𝑧 = 𝑦) ↔ (𝑧 = 𝑦𝑤 = 𝑥))
4643, 44, 453bitr4g 303 . . . . . . . . . . . . . 14 ((𝑥𝐴𝑧𝐵) → ({𝑦, 𝑥} = {𝑧, 𝑤} ↔ (𝑤 = 𝑥𝑧 = 𝑦)))
476bicomi 214 . . . . . . . . . . . . . . 15 (⟨𝑧, 𝑤⟩ ∈ 𝑔𝑧𝑔𝑤)
4847a1i 11 . . . . . . . . . . . . . 14 ((𝑥𝐴𝑧𝐵) → (⟨𝑧, 𝑤⟩ ∈ 𝑔𝑧𝑔𝑤))
4946, 48anbi12d 746 . . . . . . . . . . . . 13 ((𝑥𝐴𝑧𝐵) → (({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
5049rexbidva 3042 . . . . . . . . . . . 12 (𝑥𝐴 → (∃𝑧𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ∃𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
5150rexbidv 3045 . . . . . . . . . . 11 (𝑥𝐴 → (∃𝑤𝐴𝑧𝐵 ({𝑦, 𝑥} = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) ↔ ∃𝑤𝐴𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
5238, 51syl5bb 272 . . . . . . . . . 10 (𝑥𝐴 → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑤𝐴𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
5352adantr 481 . . . . . . . . 9 ((𝑥𝐴𝑦𝐵) → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑤𝐴𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤)))
54 breq2 4617 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝑧𝑔𝑤𝑧𝑔𝑥))
55 breq1 4616 . . . . . . . . . 10 (𝑧 = 𝑦 → (𝑧𝑔𝑥𝑦𝑔𝑥))
5654, 55ceqsrex2v 3321 . . . . . . . . 9 ((𝑥𝐴𝑦𝐵) → (∃𝑤𝐴𝑧𝐵 ((𝑤 = 𝑥𝑧 = 𝑦) ∧ 𝑧𝑔𝑤) ↔ 𝑦𝑔𝑥))
5753, 56bitrd 268 . . . . . . . 8 ((𝑥𝐴𝑦𝐵) → ({𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ 𝑦𝑔𝑥))
5857rexbidva 3042 . . . . . . 7 (𝑥𝐴 → (∃𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∃𝑦𝐵 𝑦𝑔𝑥))
5958ralbiia 2973 . . . . . 6 (∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ↔ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥)
6059biimpri 218 . . . . 5 (∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥 → ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)})
61 brdom7disj.1 . . . . . . 7 𝐴 ∈ V
62 snex 4869 . . . . . . . 8 {{𝑧, 𝑤}} ∈ V
63 simpl 473 . . . . . . . . . 10 ((𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔) → 𝑣 = {𝑧, 𝑤})
6463ss2abi 3653 . . . . . . . . 9 {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ⊆ {𝑣𝑣 = {𝑧, 𝑤}}
65 df-sn 4149 . . . . . . . . 9 {{𝑧, 𝑤}} = {𝑣𝑣 = {𝑧, 𝑤}}
6664, 65sseqtr4i 3617 . . . . . . . 8 {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ⊆ {{𝑧, 𝑤}}
6762, 66ssexi 4763 . . . . . . 7 {𝑣 ∣ (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ∈ V
6861, 1, 67ab2rexex2 7105 . . . . . 6 {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ∈ V
69 eleq2 2687 . . . . . . . . 9 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → ({𝑥, 𝑦} ∈ 𝑓 ↔ {𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
7069mobidv 2490 . . . . . . . 8 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → (∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ↔ ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
7170ralbidv 2980 . . . . . . 7 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → (∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ↔ ∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
72 eleq2 2687 . . . . . . . . 9 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → ({𝑦, 𝑥} ∈ 𝑓 ↔ {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
7372rexbidv 3045 . . . . . . . 8 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → (∃𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓 ↔ ∃𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
7473ralbidv 2980 . . . . . . 7 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → (∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓 ↔ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}))
7571, 74anbi12d 746 . . . . . 6 (𝑓 = {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} → ((∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓) ↔ (∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)})))
7668, 75spcev 3286 . . . . 5 ((∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)} ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ {𝑣 ∣ ∃𝑤𝐴𝑧𝐵 (𝑣 = {𝑧, 𝑤} ∧ ⟨𝑧, 𝑤⟩ ∈ 𝑔)}) → ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
7733, 60, 76syl2an 494 . . . 4 ((∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥) → ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
7877exlimiv 1855 . . 3 (∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥) → ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
79 preq1 4238 . . . . . . . . 9 (𝑤 = 𝑥 → {𝑤, 𝑧} = {𝑥, 𝑧})
8079eleq1d 2683 . . . . . . . 8 (𝑤 = 𝑥 → ({𝑤, 𝑧} ∈ 𝑓 ↔ {𝑥, 𝑧} ∈ 𝑓))
81 preq2 4239 . . . . . . . . 9 (𝑧 = 𝑦 → {𝑥, 𝑧} = {𝑥, 𝑦})
8281eleq1d 2683 . . . . . . . 8 (𝑧 = 𝑦 → ({𝑥, 𝑧} ∈ 𝑓 ↔ {𝑥, 𝑦} ∈ 𝑓))
83 eqid 2621 . . . . . . . 8 {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}
8416, 17, 80, 82, 83brab 4958 . . . . . . 7 (𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ {𝑥, 𝑦} ∈ 𝑓)
8584mobii 2492 . . . . . 6 (∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ ∃*𝑦{𝑥, 𝑦} ∈ 𝑓)
8685ralbii 2974 . . . . 5 (∀𝑥𝐵 ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ↔ ∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓)
87 preq1 4238 . . . . . . . . 9 (𝑤 = 𝑦 → {𝑤, 𝑧} = {𝑦, 𝑧})
8887eleq1d 2683 . . . . . . . 8 (𝑤 = 𝑦 → ({𝑤, 𝑧} ∈ 𝑓 ↔ {𝑦, 𝑧} ∈ 𝑓))
89 preq2 4239 . . . . . . . . 9 (𝑧 = 𝑥 → {𝑦, 𝑧} = {𝑦, 𝑥})
9089eleq1d 2683 . . . . . . . 8 (𝑧 = 𝑥 → ({𝑦, 𝑧} ∈ 𝑓 ↔ {𝑦, 𝑥} ∈ 𝑓))
9117, 16, 88, 90, 83brab 4958 . . . . . . 7 (𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ {𝑦, 𝑥} ∈ 𝑓)
9291rexbii 3034 . . . . . 6 (∃𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ ∃𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓)
9392ralbii 2974 . . . . 5 (∀𝑥𝐴𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥 ↔ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓)
94 df-opab 4674 . . . . . . 7 {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} = {𝑣 ∣ ∃𝑤𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)}
95 vuniex 6907 . . . . . . . 8 𝑓 ∈ V
9619prid1 4267 . . . . . . . . . . 11 𝑤 ∈ {𝑤, 𝑧}
97 elunii 4407 . . . . . . . . . . 11 ((𝑤 ∈ {𝑤, 𝑧} ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 𝑓)
9896, 97mpan 705 . . . . . . . . . 10 ({𝑤, 𝑧} ∈ 𝑓𝑤 𝑓)
9998adantl 482 . . . . . . . . 9 ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 𝑓)
10099exlimiv 1855 . . . . . . . 8 (∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑤 𝑓)
10118prid2 4268 . . . . . . . . . . 11 𝑧 ∈ {𝑤, 𝑧}
102 elunii 4407 . . . . . . . . . . 11 ((𝑧 ∈ {𝑤, 𝑧} ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑧 𝑓)
103101, 102mpan 705 . . . . . . . . . 10 ({𝑤, 𝑧} ∈ 𝑓𝑧 𝑓)
104103adantl 482 . . . . . . . . 9 ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑧 𝑓)
105 df-sn 4149 . . . . . . . . . . 11 {⟨𝑤, 𝑧⟩} = {𝑣𝑣 = ⟨𝑤, 𝑧⟩}
106 snex 4869 . . . . . . . . . . 11 {⟨𝑤, 𝑧⟩} ∈ V
107105, 106eqeltrri 2695 . . . . . . . . . 10 {𝑣𝑣 = ⟨𝑤, 𝑧⟩} ∈ V
108 simpl 473 . . . . . . . . . . 11 ((𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓) → 𝑣 = ⟨𝑤, 𝑧⟩)
109108ss2abi 3653 . . . . . . . . . 10 {𝑣 ∣ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)} ⊆ {𝑣𝑣 = ⟨𝑤, 𝑧⟩}
110107, 109ssexi 4763 . . . . . . . . 9 {𝑣 ∣ (𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V
11195, 104, 110abexex 7096 . . . . . . . 8 {𝑣 ∣ ∃𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V
11295, 100, 111abexex 7096 . . . . . . 7 {𝑣 ∣ ∃𝑤𝑧(𝑣 = ⟨𝑤, 𝑧⟩ ∧ {𝑤, 𝑧} ∈ 𝑓)} ∈ V
11394, 112eqeltri 2694 . . . . . 6 {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} ∈ V
114 breq 4615 . . . . . . . . 9 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (𝑥𝑔𝑦𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦))
115114mobidv 2490 . . . . . . . 8 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (∃*𝑦 𝑥𝑔𝑦 ↔ ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦))
116115ralbidv 2980 . . . . . . 7 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ↔ ∀𝑥𝐵 ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦))
117 breq 4615 . . . . . . . . 9 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (𝑦𝑔𝑥𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥))
118117rexbidv 3045 . . . . . . . 8 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (∃𝑦𝐵 𝑦𝑔𝑥 ↔ ∃𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥))
119118ralbidv 2980 . . . . . . 7 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → (∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥 ↔ ∀𝑥𝐴𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥))
120116, 119anbi12d 746 . . . . . 6 (𝑔 = {⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓} → ((∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥) ↔ (∀𝑥𝐵 ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥)))
121113, 120spcev 3286 . . . . 5 ((∀𝑥𝐵 ∃*𝑦 𝑥{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦{⟨𝑤, 𝑧⟩ ∣ {𝑤, 𝑧} ∈ 𝑓}𝑥) → ∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥))
12286, 93, 121syl2anbr 497 . . . 4 ((∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓) → ∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥))
123122exlimiv 1855 . . 3 (∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓) → ∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥))
12478, 123impbii 199 . 2 (∃𝑔(∀𝑥𝐵 ∃*𝑦 𝑥𝑔𝑦 ∧ ∀𝑥𝐴𝑦𝐵 𝑦𝑔𝑥) ↔ ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
1252, 124bitri 264 1 (𝐴𝐵 ↔ ∃𝑓(∀𝑥𝐵 ∃*𝑦{𝑥, 𝑦} ∈ 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 {𝑦, 𝑥} ∈ 𝑓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  ∃*wmo 2470  {cab 2607  wne 2790  wral 2907  wrex 2908  Vcvv 3186  cin 3554  c0 3891  {csn 4148  {cpr 4150  cop 4154   cuni 4402   class class class wbr 4613  {copab 4672  cdom 7897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-ac2 9229
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-card 8709  df-acn 8712  df-ac 8883
This theorem is referenced by:  grothprim  9600
  Copyright terms: Public domain W3C validator