Metamath Proof Explorer

Theorem xpider

Description: A Cartesian square is an equivalence relation (in general, it is not a poset). (Contributed by FL, 31-Jul-2009) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion xpider ( 𝐴 × 𝐴 ) Er 𝐴

Proof

Step Hyp Ref Expression
1 relxp ⊢ Rel ( 𝐴 × 𝐴 )
2 dmxpid ⊢ dom ( 𝐴 × 𝐴 ) = 𝐴
3 cnvxp ⊢ ◡ ( 𝐴 × 𝐴 ) = ( 𝐴 × 𝐴 )
4 xpidtr ⊢ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )
5 uneq1 ⊢ ( ◡ ( 𝐴 × 𝐴 ) = ( 𝐴 × 𝐴 ) → ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) )
6 unss2 ⊢ ( ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) → ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) )
7 unidm ⊢ ( ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 )
8 eqtr ⊢ ( ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) ) → ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
9 sseq2 ⊢ ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) → ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) ↔ ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝐴 × 𝐴 ) ) )
10 9 biimpd ⊢ ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) → ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) → ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝐴 × 𝐴 ) ) )
11 8 10 syl ⊢ ( ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) ) → ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) → ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝐴 × 𝐴 ) ) )
12 7 11 mpan2 ⊢ ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) = ( ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) → ( ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ◡ ( 𝐴 × 𝐴 ) ∪ ( 𝐴 × 𝐴 ) ) → ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝐴 × 𝐴 ) ) )
13 5 6 12 syl2im ⊢ ( ◡ ( 𝐴 × 𝐴 ) = ( 𝐴 × 𝐴 ) → ( ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) → ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝐴 × 𝐴 ) ) )
14 3 4 13 mp2 ⊢ ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝐴 × 𝐴 )
15 df-er ⊢ ( ( 𝐴 × 𝐴 ) Er 𝐴 ↔ ( Rel ( 𝐴 × 𝐴 ) ∧ dom ( 𝐴 × 𝐴 ) = 𝐴 ∧ ( ◡ ( 𝐴 × 𝐴 ) ∪ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝐴 × 𝐴 ) ) )
16 1 2 14 15 mpbir3an ⊢ ( 𝐴 × 𝐴 ) Er 𝐴