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

Metamath Proof Explorer

Theorem propssopi

Description: If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020) (Proof shortened by AV, 16-Jun-2022) (Avoid depending on this detail.)

Ref Expression
Hypotheses snopeqop.a ⊢ 𝐴 ∈ V
snopeqop.b ⊢ 𝐵 ∈ V
propeqop.c ⊢ 𝐶 ∈ V
propeqop.d ⊢ 𝐷 ∈ V
propeqop.e ⊢ 𝐸 ∈ V
propeqop.f ⊢ 𝐹 ∈ V
Assertion propssopi ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ⊆ ⟨ 𝐸 , 𝐹 ⟩ → 𝐴 = 𝐶 )

Proof

Step Hyp Ref Expression
1 snopeqop.a ⊢ 𝐴 ∈ V
2 snopeqop.b ⊢ 𝐵 ∈ V
3 propeqop.c ⊢ 𝐶 ∈ V
4 propeqop.d ⊢ 𝐷 ∈ V
5 propeqop.e ⊢ 𝐸 ∈ V
6 propeqop.f ⊢ 𝐹 ∈ V
7 5 6 dfop ⊢ ⟨ 𝐸 , 𝐹 ⟩ = { { 𝐸 } , { 𝐸 , 𝐹 } }
8 7 sseq2i ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ⊆ ⟨ 𝐸 , 𝐹 ⟩ ↔ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ⊆ { { 𝐸 } , { 𝐸 , 𝐹 } } )
9 sspr ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ⊆ { { 𝐸 } , { 𝐸 , 𝐹 } } ↔ ( ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ∅ ∨ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } } ) ∨ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 , 𝐹 } } ∨ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } , { 𝐸 , 𝐹 } } ) ) )
10 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
11 10 prnz ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ≠ ∅
12 eqneqall ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ∅ → ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ≠ ∅ → 𝐴 = 𝐶 ) )
13 11 12 mpi ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ∅ → 𝐴 = 𝐶 )
14 opex ⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
15 10 14 preqsn ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } } ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 } ) )
16 1 2 opth ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
17 simpl ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → 𝐴 = 𝐶 )
18 16 17 sylbi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → 𝐴 = 𝐶 )
19 18 adantr ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 } ) → 𝐴 = 𝐶 )
20 15 19 sylbi ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } } → 𝐴 = 𝐶 )
21 13 20 jaoi ⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ∅ ∨ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } } ) → 𝐴 = 𝐶 )
22 10 14 preqsn ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 , 𝐹 } } ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } ) )
23 17 a1d ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } → 𝐴 = 𝐶 ) )
24 16 23 sylbi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → ( ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } → 𝐴 = 𝐶 ) )
25 24 imp ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = { 𝐸 , 𝐹 } ) → 𝐴 = 𝐶 )
26 22 25 sylbi ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 , 𝐹 } } → 𝐴 = 𝐶 )
27 7 eqcomi ⊢ { { 𝐸 } , { 𝐸 , 𝐹 } } = ⟨ 𝐸 , 𝐹 ⟩
28 27 eqeq2i ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } , { 𝐸 , 𝐹 } } ↔ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ⟨ 𝐸 , 𝐹 ⟩ )
29 1 2 3 4 5 6 propeqop ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ⟨ 𝐸 , 𝐹 ⟩ ↔ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
30 28 29 bitri ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } , { 𝐸 , 𝐹 } } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )
31 simpll ⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) → 𝐴 = 𝐶 )
32 30 31 sylbi ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } , { 𝐸 , 𝐹 } } → 𝐴 = 𝐶 )
33 26 32 jaoi ⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 , 𝐹 } } ∨ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } , { 𝐸 , 𝐹 } } ) → 𝐴 = 𝐶 )
34 21 33 jaoi ⊢ ( ( ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ∅ ∨ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } } ) ∨ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 , 𝐹 } } ∨ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { { 𝐸 } , { 𝐸 , 𝐹 } } ) ) → 𝐴 = 𝐶 )
35 9 34 sylbi ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ⊆ { { 𝐸 } , { 𝐸 , 𝐹 } } → 𝐴 = 𝐶 )
36 8 35 sylbi ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ⊆ ⟨ 𝐸 , 𝐹 ⟩ → 𝐴 = 𝐶 )