This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exprelprel

Description: If there is an element of the set of subsets with two elements in a set, an unordered pair of sets is in the set. (Contributed by Alexander van der Vekens, 12-Jul-2018)

Ref Expression
Assertion exprelprel ( ∃ 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } 𝑝 ∈ 𝑋 → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 )

Proof

Step Hyp Ref Expression
1 elss2prb ⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) )
2 eleq1 ⊢ ( 𝑝 = { 𝑣 , 𝑤 } → ( 𝑝 ∈ 𝑋 ↔ { 𝑣 , 𝑤 } ∈ 𝑋 ) )
3 2 adantl ⊢ ( ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → ( 𝑝 ∈ 𝑋 ↔ { 𝑣 , 𝑤 } ∈ 𝑋 ) )
4 3 biimpcd ⊢ ( 𝑝 ∈ 𝑋 → ( ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → { 𝑣 , 𝑤 } ∈ 𝑋 ) )
5 4 reximdv ⊢ ( 𝑝 ∈ 𝑋 → ( ∃ 𝑤 ∈ 𝑉 ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 ) )
6 5 reximdv ⊢ ( 𝑝 ∈ 𝑋 → ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 ) )
7 6 com12 ⊢ ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → ( 𝑝 ∈ 𝑋 → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 ) )
8 1 7 sylbi ⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } → ( 𝑝 ∈ 𝑋 → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 ) )
9 8 rexlimiv ⊢ ( ∃ 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } 𝑝 ∈ 𝑋 → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 )