Users' Mathboxes 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 42249
Description: Lemma for sprsymrelf1 42254. (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 42243 . . . . . 6 ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑝𝑎) → ∃𝑖𝑉𝑗𝑉 𝑝 = {𝑖, 𝑗})
21ad4ant14 1209 . . . . 5 ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → ∃𝑖𝑉𝑗𝑉 𝑝 = {𝑖, 𝑗})
3 simpr 479 . . . . . . . . . . . . 13 (((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) → 𝑝 = {𝑖, 𝑗})
43adantr 472 . . . . . . . . . . . 12 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → 𝑝 = {𝑖, 𝑗})
54eleq1d 2822 . . . . . . . . . . 11 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (𝑝𝑎 ↔ {𝑖, 𝑗} ∈ 𝑎))
6 simpr 479 . . . . . . . . . . . . . . 15 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ {𝑖, 𝑗} ∈ 𝑎) → {𝑖, 𝑗} ∈ 𝑎)
7 eqeq1 2762 . . . . . . . . . . . . . . . 16 (𝑐 = {𝑖, 𝑗} → (𝑐 = {𝑖, 𝑗} ↔ {𝑖, 𝑗} = {𝑖, 𝑗}))
87adantl 473 . . . . . . . . . . . . . . 15 (((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ {𝑖, 𝑗} ∈ 𝑎) ∧ 𝑐 = {𝑖, 𝑗}) → (𝑐 = {𝑖, 𝑗} ↔ {𝑖, 𝑗} = {𝑖, 𝑗}))
9 eqidd 2759 . . . . . . . . . . . . . . 15 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ {𝑖, 𝑗} ∈ 𝑎) → {𝑖, 𝑗} = {𝑖, 𝑗})
106, 8, 9rspcedvd 3454 . . . . . . . . . . . . . 14 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ {𝑖, 𝑗} ∈ 𝑎) → ∃𝑐𝑎 𝑐 = {𝑖, 𝑗})
1110adantlr 753 . . . . . . . . . . . . 13 (((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) ∧ {𝑖, 𝑗} ∈ 𝑎) → ∃𝑐𝑎 𝑐 = {𝑖, 𝑗})
12 preq12 4412 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑖𝑦 = 𝑗) → {𝑥, 𝑦} = {𝑖, 𝑗})
1312eqeq2d 2768 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑐 = {𝑥, 𝑦} ↔ 𝑐 = {𝑖, 𝑗}))
1413rexbidv 3188 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑖𝑦 = 𝑗) → (∃𝑐𝑎 𝑐 = {𝑥, 𝑦} ↔ ∃𝑐𝑎 𝑐 = {𝑖, 𝑗}))
1514opelopabga 5136 . . . . . . . . . . . . . . 15 ((𝑖𝑉𝑗𝑉) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} ↔ ∃𝑐𝑎 𝑐 = {𝑖, 𝑗}))
1615bicomd 213 . . . . . . . . . . . . . 14 ((𝑖𝑉𝑗𝑉) → (∃𝑐𝑎 𝑐 = {𝑖, 𝑗} ↔ ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}}))
1716ad3antrrr 768 . . . . . . . . . . . . 13 (((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) ∧ {𝑖, 𝑗} ∈ 𝑎) → (∃𝑐𝑎 𝑐 = {𝑖, 𝑗} ↔ ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}}))
1811, 17mpbid 222 . . . . . . . . . . . 12 (((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) ∧ {𝑖, 𝑗} ∈ 𝑎) → ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}})
1918ex 449 . . . . . . . . . . 11 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → ({𝑖, 𝑗} ∈ 𝑎 → ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}}))
205, 19sylbid 230 . . . . . . . . . 10 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (𝑝𝑎 → ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}}))
21 eleq2 2826 . . . . . . . . . . . 12 ({⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} ↔ ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}))
2221ad2antll 767 . . . . . . . . . . 11 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} ↔ ⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}))
23 vex 3341 . . . . . . . . . . . . 13 𝑖 ∈ V
24 vex 3341 . . . . . . . . . . . . 13 𝑗 ∈ V
2513rexbidv 3188 . . . . . . . . . . . . . 14 ((𝑥 = 𝑖𝑦 = 𝑗) → (∃𝑐𝑏 𝑐 = {𝑥, 𝑦} ↔ ∃𝑐𝑏 𝑐 = {𝑖, 𝑗}))
2625opelopabga 5136 . . . . . . . . . . . . 13 ((𝑖 ∈ V ∧ 𝑗 ∈ V) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} ↔ ∃𝑐𝑏 𝑐 = {𝑖, 𝑗}))
2723, 24, 26mp2an 710 . . . . . . . . . . . 12 (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} ↔ ∃𝑐𝑏 𝑐 = {𝑖, 𝑗})
28 eqtr3 2779 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 = {𝑖, 𝑗} ∧ 𝑐 = {𝑖, 𝑗}) → 𝑝 = 𝑐)
2928equcomd 2099 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 = {𝑖, 𝑗} ∧ 𝑐 = {𝑖, 𝑗}) → 𝑐 = 𝑝)
3029eleq1d 2822 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 = {𝑖, 𝑗} ∧ 𝑐 = {𝑖, 𝑗}) → (𝑐𝑏𝑝𝑏))
3130biimpd 219 . . . . . . . . . . . . . . . . . . 19 ((𝑝 = {𝑖, 𝑗} ∧ 𝑐 = {𝑖, 𝑗}) → (𝑐𝑏𝑝𝑏))
3231ex 449 . . . . . . . . . . . . . . . . . 18 (𝑝 = {𝑖, 𝑗} → (𝑐 = {𝑖, 𝑗} → (𝑐𝑏𝑝𝑏)))
3332com13 88 . . . . . . . . . . . . . . . . 17 (𝑐𝑏 → (𝑐 = {𝑖, 𝑗} → (𝑝 = {𝑖, 𝑗} → 𝑝𝑏)))
3433imp 444 . . . . . . . . . . . . . . . 16 ((𝑐𝑏𝑐 = {𝑖, 𝑗}) → (𝑝 = {𝑖, 𝑗} → 𝑝𝑏))
3534rexlimiva 3164 . . . . . . . . . . . . . . 15 (∃𝑐𝑏 𝑐 = {𝑖, 𝑗} → (𝑝 = {𝑖, 𝑗} → 𝑝𝑏))
3635com12 32 . . . . . . . . . . . . . 14 (𝑝 = {𝑖, 𝑗} → (∃𝑐𝑏 𝑐 = {𝑖, 𝑗} → 𝑝𝑏))
3736adantl 473 . . . . . . . . . . . . 13 (((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) → (∃𝑐𝑏 𝑐 = {𝑖, 𝑗} → 𝑝𝑏))
3837adantr 472 . . . . . . . . . . . 12 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (∃𝑐𝑏 𝑐 = {𝑖, 𝑗} → 𝑝𝑏))
3927, 38syl5bi 232 . . . . . . . . . . 11 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} → 𝑝𝑏))
4022, 39sylbid 230 . . . . . . . . . 10 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (⟨𝑖, 𝑗⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} → 𝑝𝑏))
4120, 40syld 47 . . . . . . . . 9 ((((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) ∧ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}})) → (𝑝𝑎𝑝𝑏))
4241expimpd 630 . . . . . . . 8 (((𝑖𝑉𝑗𝑉) ∧ 𝑝 = {𝑖, 𝑗}) → ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏))
4342ex 449 . . . . . . 7 ((𝑖𝑉𝑗𝑉) → (𝑝 = {𝑖, 𝑗} → ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏)))
4443rexlimdva 3167 . . . . . 6 (𝑖𝑉 → (∃𝑗𝑉 𝑝 = {𝑖, 𝑗} → ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏)))
4544rexlimiv 3163 . . . . 5 (∃𝑖𝑉𝑗𝑉 𝑝 = {𝑖, 𝑗} → ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏))
462, 45mpcom 38 . . . 4 ((((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) ∧ 𝑝𝑎) → 𝑝𝑏)
4746ex 449 . . 3 (((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) → (𝑝𝑎𝑝𝑏))
4847ssrdv 3748 . 2 (((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}}) → 𝑎𝑏)
4948ex 449 1 ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎𝑏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1630  wcel 2137  wrex 3049  Vcvv 3338  wss 3713  {cpr 4321  cop 4325  {copab 4862  cfv 6047  Pairscspr 42235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-ral 3053  df-rex 3054  df-reu 3055  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-spr 42236
This theorem is referenced by:  sprsymrelf1  42254
  Copyright terms: Public domain W3C validator