Metamath Proof Explorer

Theorem sprsymrelf1lem

Description: Lemma for sprsymrelf1 . (Contributed by AV, 22-Nov-2021)

Ref Expression
Assertion sprsymrelf1lem ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → 𝑎 ⊆ 𝑏 ) )

Proof

Step Hyp Ref Expression
1 prssspr ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑝 ∈ 𝑎 ) → ∃ 𝑖 ∈ 𝑉 ∃ 𝑗 ∈ 𝑉 𝑝 = { 𝑖 , 𝑗 } )
2 1 ad4ant14 ⊢ ( ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ∧ 𝑝 ∈ 𝑎 ) → ∃ 𝑖 ∈ 𝑉 ∃ 𝑗 ∈ 𝑉 𝑝 = { 𝑖 , 𝑗 } )
3 simpr ⊢ ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑝 = { 𝑖 , 𝑗 } )
4 3 adantr ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → 𝑝 = { 𝑖 , 𝑗 } )
5 4 eleq1d ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → ( 𝑝 ∈ 𝑎 ↔ { 𝑖 , 𝑗 } ∈ 𝑎 ) )
6 simpr ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ { 𝑖 , 𝑗 } ∈ 𝑎 ) → { 𝑖 , 𝑗 } ∈ 𝑎 )
7 eqeq1 ⊢ ( 𝑐 = { 𝑖 , 𝑗 } → ( 𝑐 = { 𝑖 , 𝑗 } ↔ { 𝑖 , 𝑗 } = { 𝑖 , 𝑗 } ) )
8 7 adantl ⊢ ( ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ { 𝑖 , 𝑗 } ∈ 𝑎 ) ∧ 𝑐 = { 𝑖 , 𝑗 } ) → ( 𝑐 = { 𝑖 , 𝑗 } ↔ { 𝑖 , 𝑗 } = { 𝑖 , 𝑗 } ) )
9 eqidd ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ { 𝑖 , 𝑗 } ∈ 𝑎 ) → { 𝑖 , 𝑗 } = { 𝑖 , 𝑗 } )
10 6 8 9 rspcedvd ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ { 𝑖 , 𝑗 } ∈ 𝑎 ) → ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑖 , 𝑗 } )
11 10 adantlr ⊢ ( ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) ∧ { 𝑖 , 𝑗 } ∈ 𝑎 ) → ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑖 , 𝑗 } )
12 preq12 ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → { 𝑥 , 𝑦 } = { 𝑖 , 𝑗 } )
13 12 eqeq2d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑐 = { 𝑥 , 𝑦 } ↔ 𝑐 = { 𝑖 , 𝑗 } ) )
14 13 rexbidv ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } ↔ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑖 , 𝑗 } ) )
15 14 opelopabga ⊢ ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) → ( ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } ↔ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑖 , 𝑗 } ) )
16 15 bicomd ⊢ ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑖 , 𝑗 } ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } ) )
17 16 ad3antrrr ⊢ ( ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) ∧ { 𝑖 , 𝑗 } ∈ 𝑎 ) → ( ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑖 , 𝑗 } ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } ) )
18 11 17 mpbid ⊢ ( ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) ∧ { 𝑖 , 𝑗 } ∈ 𝑎 ) → ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } )
19 18 ex ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → ( { 𝑖 , 𝑗 } ∈ 𝑎 → ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } ) )
20 5 19 sylbid ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → ( 𝑝 ∈ 𝑎 → ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } ) )
21 eleq2 ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → ( ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) )
22 21 ad2antll ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → ( ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) )
23 13 rexbidv ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } ↔ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑖 , 𝑗 } ) )
24 23 opelopabga ⊢ ( ( 𝑖 ∈ V ∧ 𝑗 ∈ V ) → ( ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ↔ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑖 , 𝑗 } ) )
25 24 el2v ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ↔ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑖 , 𝑗 } )
26 eqtr3 ⊢ ( ( 𝑝 = { 𝑖 , 𝑗 } ∧ 𝑐 = { 𝑖 , 𝑗 } ) → 𝑝 = 𝑐 )
27 26 equcomd ⊢ ( ( 𝑝 = { 𝑖 , 𝑗 } ∧ 𝑐 = { 𝑖 , 𝑗 } ) → 𝑐 = 𝑝 )
28 27 eleq1d ⊢ ( ( 𝑝 = { 𝑖 , 𝑗 } ∧ 𝑐 = { 𝑖 , 𝑗 } ) → ( 𝑐 ∈ 𝑏 ↔ 𝑝 ∈ 𝑏 ) )
29 28 biimpd ⊢ ( ( 𝑝 = { 𝑖 , 𝑗 } ∧ 𝑐 = { 𝑖 , 𝑗 } ) → ( 𝑐 ∈ 𝑏 → 𝑝 ∈ 𝑏 ) )
30 29 ex ⊢ ( 𝑝 = { 𝑖 , 𝑗 } → ( 𝑐 = { 𝑖 , 𝑗 } → ( 𝑐 ∈ 𝑏 → 𝑝 ∈ 𝑏 ) ) )
31 30 com13 ⊢ ( 𝑐 ∈ 𝑏 → ( 𝑐 = { 𝑖 , 𝑗 } → ( 𝑝 = { 𝑖 , 𝑗 } → 𝑝 ∈ 𝑏 ) ) )
32 31 imp ⊢ ( ( 𝑐 ∈ 𝑏 ∧ 𝑐 = { 𝑖 , 𝑗 } ) → ( 𝑝 = { 𝑖 , 𝑗 } → 𝑝 ∈ 𝑏 ) )
33 32 rexlimiva ⊢ ( ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑖 , 𝑗 } → ( 𝑝 = { 𝑖 , 𝑗 } → 𝑝 ∈ 𝑏 ) )
34 33 com12 ⊢ ( 𝑝 = { 𝑖 , 𝑗 } → ( ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑖 , 𝑗 } → 𝑝 ∈ 𝑏 ) )
35 34 adantl ⊢ ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → ( ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑖 , 𝑗 } → 𝑝 ∈ 𝑏 ) )
36 35 adantr ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → ( ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑖 , 𝑗 } → 𝑝 ∈ 𝑏 ) )
37 25 36 syl5bi ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → ( ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → 𝑝 ∈ 𝑏 ) )
38 22 37 sylbid ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → ( ⟨ 𝑖 , 𝑗 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } → 𝑝 ∈ 𝑏 ) )
39 20 38 syld ⊢ ( ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) ∧ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ) → ( 𝑝 ∈ 𝑎 → 𝑝 ∈ 𝑏 ) )
40 39 expimpd ⊢ ( ( ( 𝑖 ∈ 𝑉 ∧ 𝑗 ∈ 𝑉 ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → ( ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ∧ 𝑝 ∈ 𝑎 ) → 𝑝 ∈ 𝑏 ) )
41 40 rexlimdva2 ⊢ ( 𝑖 ∈ 𝑉 → ( ∃ 𝑗 ∈ 𝑉 𝑝 = { 𝑖 , 𝑗 } → ( ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ∧ 𝑝 ∈ 𝑎 ) → 𝑝 ∈ 𝑏 ) ) )
42 41 rexlimiv ⊢ ( ∃ 𝑖 ∈ 𝑉 ∃ 𝑗 ∈ 𝑉 𝑝 = { 𝑖 , 𝑗 } → ( ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ∧ 𝑝 ∈ 𝑎 ) → 𝑝 ∈ 𝑏 ) )
43 2 42 mpcom ⊢ ( ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) ∧ 𝑝 ∈ 𝑎 ) → 𝑝 ∈ 𝑏 )
44 43 ex ⊢ ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) → ( 𝑝 ∈ 𝑎 → 𝑝 ∈ 𝑏 ) )
45 44 ssrdv ⊢ ( ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } ) → 𝑎 ⊆ 𝑏 )
46 45 ex ⊢ ( ( 𝑎 ⊆ ( Pairs ‘ 𝑉 ) ∧ 𝑏 ⊆ ( Pairs ‘ 𝑉 ) ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑎 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑏 𝑐 = { 𝑥 , 𝑦 } } → 𝑎 ⊆ 𝑏 ) )