Metamath Proof Explorer

Theorem marypha2lem3

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

Ref Expression
Hypothesis marypha2lem.t ⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) )
Assertion marypha2lem3 ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐺 ⊆ 𝑇 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 marypha2lem.t ⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) )
2 dffn5 ⊢ ( 𝐺 Fn 𝐴 ↔ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) )
3 2 biimpi ⊢ ( 𝐺 Fn 𝐴 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) )
4 3 adantl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) )
5 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) }
6 4 5 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } )
7 1 marypha2lem2 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
8 7 a1i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
9 6 8 sseq12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐺 ⊆ 𝑇 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ) )
10 ssopab2bw ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
11 9 10 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐺 ⊆ 𝑇 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ) )
12 19.21v ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
13 imdistan ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
14 13 albii ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
15 fvex ⊢ ( 𝐺 ‘ 𝑥 ) ∈ V
16 eleq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
17 15 16 ceqsalv ⊢ ( ∀ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
18 17 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
19 12 14 18 3bitr3i ⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
20 19 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
21 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
22 20 21 bitr4i ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
23 11 22 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐺 ⊆ 𝑇 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )