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 eqtrid ( ( 𝐹 Fn 𝐴𝑋𝐴 ) → ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝑋𝑦 ∈ ( 𝐹𝑥 ) ) } = 𝑥𝑋 ( 𝐹𝑥 ) )
17 8 16 eqtrd ( ( 𝐹 Fn 𝐴𝑋𝐴 ) → ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝐹𝑥 ) ) } ↾ 𝑋 ) = 𝑥𝑋 ( 𝐹𝑥 ) )
18 5 17 eqtrid ( ( 𝐹 Fn 𝐴𝑋𝐴 ) → ( 𝑇𝑋 ) = 𝑥𝑋 ( 𝐹𝑥 ) )
19 fnfun ( 𝐹 Fn 𝐴 → Fun 𝐹 )
20 19 adantr ( ( 𝐹 Fn 𝐴𝑋𝐴 ) → Fun 𝐹 )
21 funiunfv ( Fun 𝐹 𝑥𝑋 ( 𝐹𝑥 ) = ( 𝐹𝑋 ) )
22 20 21 syl ( ( 𝐹 Fn 𝐴𝑋𝐴 ) → 𝑥𝑋 ( 𝐹𝑥 ) = ( 𝐹𝑋 ) )
23 18 22 eqtrd ( ( 𝐹 Fn 𝐴𝑋𝐴 ) → ( 𝑇𝑋 ) = ( 𝐹𝑋 ) )