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 bilani ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) )
4 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) }
5 3 4 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } )
6 1 marypha2lem2 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
7 6 a1i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
8 5 7 sseq12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐺 ⊆ 𝑇 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ) )
9 ssopab2bw ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
10 8 9 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐺 ⊆ 𝑇 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ) )
11 19.21v ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
12 imdistan ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
13 12 albii ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
14 fvex ⊢ ( 𝐺 ‘ 𝑥 ) ∈ V
15 eleq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
16 14 15 ceqsalv ⊢ ( ∀ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
17 16 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
18 11 13 17 3bitr3i ⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
19 18 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
20 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
21 19 20 bitr4i ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
22 10 21 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐺 ⊆ 𝑇 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )