Metamath Proof Explorer

Theorem sprsymrelfolem2

Description: Lemma 2 for sprsymrelfo . (Contributed by AV, 23-Nov-2021)

Ref Expression
Hypothesis sprsymrelfo.q ⊢ 𝑄 = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) }
Assertion sprsymrelfolem2 ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → ( 𝑥 𝑅 𝑦 ↔ ∃ 𝑐 ∈ 𝑄 𝑐 = { 𝑥 , 𝑦 } ) )

Proof

Step Hyp Ref Expression
1 sprsymrelfo.q ⊢ 𝑄 = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) }
2 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
3 simpl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ) → 𝑉 ∈ 𝑊 )
4 ssel ⊢ ( 𝑅 ⊆ ( 𝑉 × 𝑉 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ) )
5 4 adantl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ) )
6 5 imp ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) )
7 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
8 6 7 sylib ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
9 prelspr ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) )
10 3 8 9 syl2an2r ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) → { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) )
11 10 ex ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) ) )
12 2 11 syl5bi ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ) → ( 𝑥 𝑅 𝑦 → { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) ) )
13 12 3adant3 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → ( 𝑥 𝑅 𝑦 → { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) ) )
14 13 imp ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) → { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) )
15 vex ⊢ 𝑥 ∈ V
16 vex ⊢ 𝑦 ∈ V
17 vex ⊢ 𝑎 ∈ V
18 vex ⊢ 𝑏 ∈ V
19 15 16 17 18 preq12b ⊢ ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ↔ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ) )
20 breq12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑎 𝑅 𝑏 ) )
21 20 biimpd ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 𝑅 𝑦 → 𝑎 𝑅 𝑏 ) )
22 21 com12 ⊢ ( 𝑥 𝑅 𝑦 → ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑎 𝑅 𝑏 ) )
23 22 adantl ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑎 𝑅 𝑏 ) )
24 23 adantr ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑎 𝑅 𝑏 ) )
25 24 com12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 𝑅 𝑏 ) )
26 rsp2 ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )
27 26 ancomsd ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) → ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )
28 27 imp ⊢ ( ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) )
29 28 biimpd ⊢ ( ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
30 29 ex ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) → ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
31 30 3ad2ant3 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
32 31 com23 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → ( 𝑥 𝑅 𝑦 → ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → 𝑦 𝑅 𝑥 ) ) )
33 32 imp ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → 𝑦 𝑅 𝑥 ) )
34 33 adantl ⊢ ( ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ∧ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ) → ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → 𝑦 𝑅 𝑥 ) )
35 eleq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ∈ 𝑉 ↔ 𝑎 ∈ 𝑉 ) )
36 eleq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 ∈ 𝑉 ↔ 𝑏 ∈ 𝑉 ) )
37 35 36 bi2anan9r ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ↔ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
38 breq12 ⊢ ( ( 𝑦 = 𝑎 ∧ 𝑥 = 𝑏 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑎 𝑅 𝑏 ) )
39 38 ancoms ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑎 𝑅 𝑏 ) )
40 37 39 imbi12d ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → 𝑦 𝑅 𝑥 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → 𝑎 𝑅 𝑏 ) ) )
41 40 adantr ⊢ ( ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ∧ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ) → ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → 𝑦 𝑅 𝑥 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → 𝑎 𝑅 𝑏 ) ) )
42 34 41 mpbid ⊢ ( ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ∧ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → 𝑎 𝑅 𝑏 ) )
43 42 expimpd ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) → ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 𝑅 𝑏 ) )
44 25 43 jaoi ⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ) → ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 𝑅 𝑏 ) )
45 44 com12 ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑎 ) ) → 𝑎 𝑅 𝑏 ) )
46 19 45 syl5bi ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) )
47 46 ralrimivva ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) )
48 1 eleq2i ⊢ ( { 𝑥 , 𝑦 } ∈ 𝑄 ↔ { 𝑥 , 𝑦 } ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) } )
49 eqeq1 ⊢ ( 𝑞 = { 𝑥 , 𝑦 } → ( 𝑞 = { 𝑎 , 𝑏 } ↔ { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) )
50 49 imbi1d ⊢ ( 𝑞 = { 𝑥 , 𝑦 } → ( ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ↔ ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) )
51 50 2ralbidv ⊢ ( 𝑞 = { 𝑥 , 𝑦 } → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) )
52 51 elrab ⊢ ( { 𝑥 , 𝑦 } ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) } ↔ ( { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) )
53 48 52 bitri ⊢ ( { 𝑥 , 𝑦 } ∈ 𝑄 ↔ ( { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) )
54 14 47 53 sylanbrc ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) → { 𝑥 , 𝑦 } ∈ 𝑄 )
55 eqidd ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) → { 𝑥 , 𝑦 } = { 𝑥 , 𝑦 } )
56 eqeq1 ⊢ ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑐 = { 𝑥 , 𝑦 } ↔ { 𝑥 , 𝑦 } = { 𝑥 , 𝑦 } ) )
57 56 rspcev ⊢ ( ( { 𝑥 , 𝑦 } ∈ 𝑄 ∧ { 𝑥 , 𝑦 } = { 𝑥 , 𝑦 } ) → ∃ 𝑐 ∈ 𝑄 𝑐 = { 𝑥 , 𝑦 } )
58 54 55 57 syl2anc ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑐 ∈ 𝑄 𝑐 = { 𝑥 , 𝑦 } )
59 58 ex ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → ( 𝑥 𝑅 𝑦 → ∃ 𝑐 ∈ 𝑄 𝑐 = { 𝑥 , 𝑦 } ) )
60 1 eleq2i ⊢ ( 𝑐 ∈ 𝑄 ↔ 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) } )
61 eqeq1 ⊢ ( 𝑞 = 𝑐 → ( 𝑞 = { 𝑎 , 𝑏 } ↔ 𝑐 = { 𝑎 , 𝑏 } ) )
62 61 imbi1d ⊢ ( 𝑞 = 𝑐 → ( ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ↔ ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) )
63 62 2ralbidv ⊢ ( 𝑞 = 𝑐 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) )
64 63 elrab ⊢ ( 𝑐 ∈ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) } ↔ ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) )
65 60 64 bitri ⊢ ( 𝑐 ∈ 𝑄 ↔ ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) )
66 eleq1 ⊢ ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) ↔ { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) ) )
67 prsprel ⊢ ( ( { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
68 15 16 67 mpanr12 ⊢ ( { 𝑥 , 𝑦 } ∈ ( Pairs ‘ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
69 66 68 syl6bi ⊢ ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
70 69 com12 ⊢ ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) → ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
71 70 adantr ⊢ ( ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) → ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
72 71 imp ⊢ ( ( ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) ∧ 𝑐 = { 𝑥 , 𝑦 } ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
73 preq1 ⊢ ( 𝑎 = 𝑥 → { 𝑎 , 𝑏 } = { 𝑥 , 𝑏 } )
74 73 eqeq2d ⊢ ( 𝑎 = 𝑥 → ( 𝑐 = { 𝑎 , 𝑏 } ↔ 𝑐 = { 𝑥 , 𝑏 } ) )
75 breq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 𝑅 𝑏 ↔ 𝑥 𝑅 𝑏 ) )
76 74 75 imbi12d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ↔ ( 𝑐 = { 𝑥 , 𝑏 } → 𝑥 𝑅 𝑏 ) ) )
77 preq2 ⊢ ( 𝑏 = 𝑦 → { 𝑥 , 𝑏 } = { 𝑥 , 𝑦 } )
78 77 eqeq2d ⊢ ( 𝑏 = 𝑦 → ( 𝑐 = { 𝑥 , 𝑏 } ↔ 𝑐 = { 𝑥 , 𝑦 } ) )
79 breq2 ⊢ ( 𝑏 = 𝑦 → ( 𝑥 𝑅 𝑏 ↔ 𝑥 𝑅 𝑦 ) )
80 78 79 imbi12d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑐 = { 𝑥 , 𝑏 } → 𝑥 𝑅 𝑏 ) ↔ ( 𝑐 = { 𝑥 , 𝑦 } → 𝑥 𝑅 𝑦 ) ) )
81 76 80 rspc2v ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) → ( 𝑐 = { 𝑥 , 𝑦 } → 𝑥 𝑅 𝑦 ) ) )
82 81 a1d ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) → ( 𝑐 = { 𝑥 , 𝑦 } → 𝑥 𝑅 𝑦 ) ) ) )
83 82 imp4c ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) ∧ 𝑐 = { 𝑥 , 𝑦 } ) → 𝑥 𝑅 𝑦 ) )
84 72 83 mpcom ⊢ ( ( ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) ∧ 𝑐 = { 𝑥 , 𝑦 } ) → 𝑥 𝑅 𝑦 )
85 84 a1d ⊢ ( ( ( 𝑐 ∈ ( Pairs ‘ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑐 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) ) ∧ 𝑐 = { 𝑥 , 𝑦 } ) → ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → 𝑥 𝑅 𝑦 ) )
86 65 85 sylanb ⊢ ( ( 𝑐 ∈ 𝑄 ∧ 𝑐 = { 𝑥 , 𝑦 } ) → ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → 𝑥 𝑅 𝑦 ) )
87 86 rexlimiva ⊢ ( ∃ 𝑐 ∈ 𝑄 𝑐 = { 𝑥 , 𝑦 } → ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → 𝑥 𝑅 𝑦 ) )
88 87 com12 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → ( ∃ 𝑐 ∈ 𝑄 𝑐 = { 𝑥 , 𝑦 } → 𝑥 𝑅 𝑦 ) )
89 59 88 impbid ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ ( 𝑉 × 𝑉 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) → ( 𝑥 𝑅 𝑦 ↔ ∃ 𝑐 ∈ 𝑄 𝑐 = { 𝑥 , 𝑦 } ) )