Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sprsymrelf1lem Structured version   Visualization version   GIF version

Theorem sprsymrelf1lem 44366
 Description: Lemma for sprsymrelf1 44371. (Contributed by AV, 22-Nov-2021.)
Assertion
Ref Expression
sprsymrelf1lem ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎𝑏))
Distinct variable groups:   𝑉,𝑐   𝑎,𝑏,𝑐,𝑥,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem sprsymrelf1lem
Dummy variables 𝑝 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prssspr 44360 . . . . . 6 ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑝𝑎) → ∃𝑖𝑉𝑗𝑉 𝑝 = {𝑖, 𝑗})
21ad4ant14 752 . . . . 5 ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → ∃𝑖𝑉𝑗𝑉 𝑝 = {𝑖, 𝑗})
3 simpr 489 . . . . . . . . . . . 12 (((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑝 = {𝑖, 𝑗})
43adantr 485 . . . . . . . . . . 11 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → 𝑝 = {𝑖, 𝑗})
54eleq1d 2837 . . . . . . . . . 10 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (𝑝𝑎 ↔ {𝑖, 𝑗} ∈ 𝑎))
6 simpr 489 . . . . . . . . . . . . . 14 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ {𝑖, 𝑗} ∈ 𝑎) → {𝑖, 𝑗} ∈ 𝑎)
7 eqeq1 2763 . . . . . . . . . . . . . . 15 (𝑐 = {𝑖, 𝑗} → (𝑐 = {𝑖, 𝑗} ↔ {𝑖, 𝑗} = {𝑖, 𝑗}))
87adantl 486 . . . . . . . . . . . . . 14 (((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ {𝑖, 𝑗} ∈ 𝑎) ∧ 𝑐 = {𝑖, 𝑗}) → (𝑐 = {𝑖, 𝑗} ↔ {𝑖, 𝑗} = {𝑖, 𝑗}))
9 eqidd 2760 . . . . . . . . . . . . . 14 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ {𝑖, 𝑗} ∈ 𝑎) → {𝑖, 𝑗} = {𝑖, 𝑗})
106, 8, 9rspcedvd 3545 . . . . . . . . . . . . 13 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ {𝑖, 𝑗} ∈ 𝑎) → ∃𝑐𝑎 𝑐 = {𝑖, 𝑗})
1110adantlr 715 . . . . . . . . . . . 12 (((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) ∧ {𝑖, 𝑗} ∈ 𝑎) → ∃𝑐𝑎 𝑐 = {𝑖, 𝑗})
12 preq12 4626 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑖𝑦 = 𝑗) → {𝑥, 𝑦} = {𝑖, 𝑗})
1312eqeq2d 2770 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑐 = {𝑥, 𝑦} ↔ 𝑐 = {𝑖, 𝑗}))
1413rexbidv 3222 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑖𝑦 = 𝑗) → (∃𝑐𝑎 𝑐 = {𝑥, 𝑦} ↔ ∃𝑐𝑎 𝑐 = {𝑖, 𝑗}))
1514opelopabga 5388 . . . . . . . . . . . . . 14 ((𝑖𝑉𝑗𝑉) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} ↔ ∃𝑐𝑎 𝑐 = {𝑖, 𝑗}))
1615bicomd 226 . . . . . . . . . . . . 13 ((𝑖𝑉𝑗𝑉) → (∃𝑐𝑎 𝑐 = {𝑖, 𝑗} ↔ ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}}))
1716ad3antrrr 730 . . . . . . . . . . . 12 (((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) ∧ {𝑖, 𝑗} ∈ 𝑎) → (∃𝑐𝑎 𝑐 = {𝑖, 𝑗} ↔ ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}}))
1811, 17mpbid 235 . . . . . . . . . . 11 (((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) ∧ {𝑖, 𝑗} ∈ 𝑎) → ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}})
1918ex 417 . . . . . . . . . 10 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → ({𝑖, 𝑗} ∈ 𝑎 → ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}}))
205, 19sylbid 243 . . . . . . . . 9 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (𝑝𝑎 → ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}}))
21 eleq2 2841 . . . . . . . . . . 11 ({⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} ↔ ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}))
2221ad2antll 729 . . . . . . . . . 10 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} ↔ ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}))
2313rexbidv 3222 . . . . . . . . . . . . 13 ((𝑥 = 𝑖𝑦 = 𝑗) → (∃𝑐𝑏 𝑐 = {𝑥, 𝑦} ↔ ∃𝑐𝑏 𝑐 = {𝑖, 𝑗}))
2423opelopabga 5388 . . . . . . . . . . . 12 ((𝑖 ∈ V ∧ 𝑗 ∈ V) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} ↔ ∃𝑐𝑏 𝑐 = {𝑖, 𝑗}))
2524el2v 3418 . . . . . . . . . . 11 (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} ↔ ∃𝑐𝑏 𝑐 = {𝑖, 𝑗})
26 eqtr3 2781 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 = {𝑖, 𝑗} ∧ 𝑐 = {𝑖, 𝑗}) → 𝑝 = 𝑐)
2726equcomd 2027 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = {𝑖, 𝑗} ∧ 𝑐 = {𝑖, 𝑗}) → 𝑐 = 𝑝)
2827eleq1d 2837 . . . . . . . . . . . . . . . . . . 19 ((𝑝 = {𝑖, 𝑗} ∧ 𝑐 = {𝑖, 𝑗}) → (𝑐𝑏𝑝𝑏))
2928biimpd 232 . . . . . . . . . . . . . . . . . 18 ((𝑝 = {𝑖, 𝑗} ∧ 𝑐 = {𝑖, 𝑗}) → (𝑐𝑏𝑝𝑏))
3029ex 417 . . . . . . . . . . . . . . . . 17 (𝑝 = {𝑖, 𝑗} → (𝑐 = {𝑖, 𝑗} → (𝑐𝑏𝑝𝑏)))
3130com13 88 . . . . . . . . . . . . . . . 16 (𝑐𝑏 → (𝑐 = {𝑖, 𝑗} → (𝑝 = {𝑖, 𝑗} → 𝑝𝑏)))
3231imp 411 . . . . . . . . . . . . . . 15 ((𝑐𝑏𝑐 = {𝑖, 𝑗}) → (𝑝 = {𝑖, 𝑗} → 𝑝𝑏))
3332rexlimiva 3206 . . . . . . . . . . . . . 14 (∃𝑐𝑏 𝑐 = {𝑖, 𝑗} → (𝑝 = {𝑖, 𝑗} → 𝑝𝑏))
3433com12 32 . . . . . . . . . . . . 13 (𝑝 = {𝑖, 𝑗} → (∃𝑐𝑏 𝑐 = {𝑖, 𝑗} → 𝑝𝑏))
3534adantl 486 . . . . . . . . . . . 12 (((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) → (∃𝑐𝑏 𝑐 = {𝑖, 𝑗} → 𝑝𝑏))
3635adantr 485 . . . . . . . . . . 11 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (∃𝑐𝑏 𝑐 = {𝑖, 𝑗} → 𝑝𝑏))
3725, 36syl5bi 245 . . . . . . . . . 10 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} → 𝑝𝑏))
3822, 37sylbid 243 . . . . . . . . 9 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} → 𝑝𝑏))
3920, 38syld 47 . . . . . . . 8 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (𝑝𝑎𝑝𝑏))
4039expimpd 458 . . . . . . 7 (((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) → ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏))
4140rexlimdva2 3212 . . . . . 6 (𝑖𝑉 → (∃𝑗𝑉 𝑝 = {𝑖, 𝑗} → ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏)))
4241rexlimiv 3205 . . . . 5 (∃𝑖𝑉𝑗𝑉 𝑝 = {𝑖, 𝑗} → ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏))
432, 42mpcom 38 . . . 4 ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏)
4443ex 417 . . 3 (((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) → (𝑝𝑎𝑝𝑏))
4544ssrdv 3899 . 2 (((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) → 𝑎𝑏)
4645ex 417 1 ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎𝑏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∃wrex 3072  Vcvv 3410   ⊆ wss 3859  {cpr 4522  ⟨cop 4526  {copab 5092  ‘cfv 6333  Pairscspr 44352 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7457 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-op 4527  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5428  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-spr 44353 This theorem is referenced by:  sprsymrelf1  44371
 Copyright terms: Public domain W3C validator