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

Metamath Proof Explorer

Theorem marypha2lem2

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

Ref Expression
Hypothesis marypha2lem.t ⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) )
Assertion marypha2lem2 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }

Proof

Step Hyp Ref Expression
1 marypha2lem.t ⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) )
2 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
3 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
4 2 3 xpeq12d ⊢ ( 𝑥 = 𝑧 → ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) ) = ( { 𝑧 } × ( 𝐹 ‘ 𝑧 ) ) )
5 4 cbviunv ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) ) = ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ( 𝐹 ‘ 𝑧 ) )
6 df-xp ⊢ ( { 𝑧 } × ( 𝐹 ‘ 𝑧 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) }
7 6 a1i ⊢ ( 𝑧 ∈ 𝐴 → ( { 𝑧 } × ( 𝐹 ‘ 𝑧 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) } )
8 7 iuneq2i ⊢ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ( 𝐹 ‘ 𝑧 ) ) = ∪ 𝑧 ∈ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) }
9 iunopab ⊢ ∪ 𝑧 ∈ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) }
10 velsn ⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑥 = 𝑧 )
11 equcom ⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
12 10 11 bitri ⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑧 = 𝑥 )
13 12 anbi1i ⊢ ( ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) ↔ ( 𝑧 = 𝑥 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) )
14 13 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑧 = 𝑥 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) )
15 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
16 15 eleq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
17 16 ceqsrexbv ⊢ ( ∃ 𝑧 ∈ 𝐴 ( 𝑧 = 𝑥 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
18 14 17 bitri ⊢ ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
19 18 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∈ { 𝑧 } ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
20 8 9 19 3eqtri ⊢ ∪ 𝑧 ∈ 𝐴 ( { 𝑧 } × ( 𝐹 ‘ 𝑧 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
21 1 5 20 3eqtri ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }