Metamath Proof Explorer


Theorem sprsymrelfvlem

Description: Lemma for sprsymrelf and sprsymrelfv . (Contributed by AV, 19-Nov-2021)

Ref Expression
Assertion sprsymrelfvlem ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → 𝑉 ∈ V )
2 eleq1 ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑐𝑃 ↔ { 𝑥 , 𝑦 } ∈ 𝑃 ) )
3 prsssprel ( ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ∧ { 𝑥 , 𝑦 } ∈ 𝑃 ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥𝑉𝑦𝑉 ) )
4 3 3exp ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( { 𝑥 , 𝑦 } ∈ 𝑃 → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥𝑉𝑦𝑉 ) ) ) )
5 4 com13 ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( { 𝑥 , 𝑦 } ∈ 𝑃 → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥𝑉𝑦𝑉 ) ) ) )
6 5 el2v ( { 𝑥 , 𝑦 } ∈ 𝑃 → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥𝑉𝑦𝑉 ) ) )
7 2 6 syl6bi ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑐𝑃 → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥𝑉𝑦𝑉 ) ) ) )
8 7 com12 ( 𝑐𝑃 → ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥𝑉𝑦𝑉 ) ) ) )
9 8 rexlimiv ( ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥𝑉𝑦𝑉 ) ) )
10 9 com12 ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } → ( 𝑥𝑉𝑦𝑉 ) ) )
11 10 adantl ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → ( ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } → ( 𝑥𝑉𝑦𝑉 ) ) )
12 11 imp ( ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( 𝑥𝑉𝑦𝑉 ) )
13 12 simpld ( ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) → 𝑥𝑉 )
14 12 simprd ( ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) → 𝑦𝑉 )
15 1 1 13 14 opabex2 ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ V )
16 elopab ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ↔ ∃ 𝑥𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) )
17 9 adantl ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥𝑉𝑦𝑉 ) ) )
18 17 adantld ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → ( 𝑥𝑉𝑦𝑉 ) ) )
19 18 imp ( ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) ∧ ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ) → ( 𝑥𝑉𝑦𝑉 ) )
20 eleq1 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ∈ ( 𝑉 × 𝑉 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ) )
21 20 ad2antrr ( ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) ∧ ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ) → ( 𝑝 ∈ ( 𝑉 × 𝑉 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ) )
22 opelxp ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝑥𝑉𝑦𝑉 ) )
23 21 22 bitrdi ( ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) ∧ ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ) → ( 𝑝 ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝑥𝑉𝑦𝑉 ) ) )
24 19 23 mpbird ( ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) ∧ ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ) → 𝑝 ∈ ( 𝑉 × 𝑉 ) )
25 24 ex ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → 𝑝 ∈ ( 𝑉 × 𝑉 ) ) )
26 25 exlimivv ( ∃ 𝑥𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → 𝑝 ∈ ( 𝑉 × 𝑉 ) ) )
27 16 26 sylbi ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } → ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → 𝑝 ∈ ( 𝑉 × 𝑉 ) ) )
28 27 com12 ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } → 𝑝 ∈ ( 𝑉 × 𝑉 ) ) )
29 28 ssrdv ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ⊆ ( 𝑉 × 𝑉 ) )
30 15 29 elpwd ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )
31 30 ex ( 𝑉 ∈ V → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) ) )
32 fvprc ( ¬ 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) = ∅ )
33 32 sseq2d ( ¬ 𝑉 ∈ V → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ↔ 𝑃 ⊆ ∅ ) )
34 ss0b ( 𝑃 ⊆ ∅ ↔ 𝑃 = ∅ )
35 33 34 bitrdi ( ¬ 𝑉 ∈ V → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ↔ 𝑃 = ∅ ) )
36 rex0 ¬ ∃ 𝑐 ∈ ∅ 𝑐 = { 𝑥 , 𝑦 }
37 rexeq ( 𝑃 = ∅ → ( ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } ↔ ∃ 𝑐 ∈ ∅ 𝑐 = { 𝑥 , 𝑦 } ) )
38 36 37 mtbiri ( 𝑃 = ∅ → ¬ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } )
39 38 alrimivv ( 𝑃 = ∅ → ∀ 𝑥𝑦 ¬ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } )
40 opab0 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } = ∅ ↔ ∀ 𝑥𝑦 ¬ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } )
41 39 40 sylibr ( 𝑃 = ∅ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } = ∅ )
42 0elpw ∅ ∈ 𝒫 ( 𝑉 × 𝑉 )
43 41 42 eqeltrdi ( 𝑃 = ∅ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )
44 35 43 syl6bi ( ¬ 𝑉 ∈ V → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) ) )
45 31 44 pm2.61i ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )