Metamath Proof Explorer

Theorem marypha2lem4

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

Ref Expression
Hypothesis marypha2lem.t ⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) )
Assertion marypha2lem4 ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑇 “ 𝑋 ) = ∪ ( 𝐹 “ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 marypha2lem.t ⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) )
2 1 marypha2lem2 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
3 2 imaeq1i ⊢ ( 𝑇 “ 𝑋 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } “ 𝑋 )
4 df-ima ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } “ 𝑋 ) = ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↾ 𝑋 )
5 3 4 eqtri ⊢ ( 𝑇 “ 𝑋 ) = ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↾ 𝑋 )
6 resopab2 ⊢ ( 𝑋 ⊆ 𝐴 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↾ 𝑋 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
7 6 adantl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↾ 𝑋 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
8 7 rneqd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↾ 𝑋 ) = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
9 rnopab ⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
10 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑋 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
11 10 bicomi ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝑋 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
12 11 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) }
13 df-iun ⊢ ∪ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) }
14 12 13 eqtr4i ⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = ∪ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 )
15 14 a1i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = ∪ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) )
16 9 15 syl5eq ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = ∪ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) )
17 8 16 eqtrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↾ 𝑋 ) = ∪ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) )
18 5 17 syl5eq ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑇 “ 𝑋 ) = ∪ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) )
19 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
20 19 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → Fun 𝐹 )
21 funiunfv ⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ 𝑋 ) )
22 20 21 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ∪ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ 𝑋 ) )
23 18 22 eqtrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑇 “ 𝑋 ) = ∪ ( 𝐹 “ 𝑋 ) )