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

Metamath Proof Explorer

Theorem fnwelem

Description: Lemma for fnwe . (Contributed by Mario Carneiro, 10-Mar-2013) (Revised by Mario Carneiro, 18-Nov-2014)

Ref Expression
Hypotheses fnwe.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) }
fnwe.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
fnwe.3 ⊢ ( 𝜑 → 𝑅 We 𝐵 )
fnwe.4 ⊢ ( 𝜑 → 𝑆 We 𝐴 )
fnwe.5 ⊢ ( 𝜑 → ( 𝐹 “ 𝑤 ) ∈ V )
fnwelem.6 ⊢ 𝑄 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝐵 × 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ∧ ( ( 1st ‘ 𝑢 ) 𝑅 ( 1st ‘ 𝑣 ) ∨ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑣 ) ∧ ( 2nd ‘ 𝑢 ) 𝑆 ( 2nd ‘ 𝑣 ) ) ) ) }
fnwelem.7 ⊢ 𝐺 = ( 𝑧 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑧 ) , 𝑧 ⟩ )
Assertion fnwelem ( 𝜑 → 𝑇 We 𝐴 )

Proof

Step Hyp Ref Expression
1 fnwe.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) }
2 fnwe.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
3 fnwe.3 ⊢ ( 𝜑 → 𝑅 We 𝐵 )
4 fnwe.4 ⊢ ( 𝜑 → 𝑆 We 𝐴 )
5 fnwe.5 ⊢ ( 𝜑 → ( 𝐹 “ 𝑤 ) ∈ V )
6 fnwelem.6 ⊢ 𝑄 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝐵 × 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ∧ ( ( 1st ‘ 𝑢 ) 𝑅 ( 1st ‘ 𝑣 ) ∨ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑣 ) ∧ ( 2nd ‘ 𝑢 ) 𝑆 ( 2nd ‘ 𝑣 ) ) ) ) }
7 fnwelem.7 ⊢ 𝐺 = ( 𝑧 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑧 ) , 𝑧 ⟩ )
8 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
9 simpr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
10 8 9 opelxpd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑧 ) , 𝑧 ⟩ ∈ ( 𝐵 × 𝐴 ) )
11 10 7 fmptd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐺 : 𝐴 ⟶ ( 𝐵 × 𝐴 ) )
12 frn ⊢ ( 𝐺 : 𝐴 ⟶ ( 𝐵 × 𝐴 ) → ran 𝐺 ⊆ ( 𝐵 × 𝐴 ) )
13 2 11 12 3syl ⊢ ( 𝜑 → ran 𝐺 ⊆ ( 𝐵 × 𝐴 ) )
14 6 wexp ⊢ ( ( 𝑅 We 𝐵 ∧ 𝑆 We 𝐴 ) → 𝑄 We ( 𝐵 × 𝐴 ) )
15 3 4 14 syl2anc ⊢ ( 𝜑 → 𝑄 We ( 𝐵 × 𝐴 ) )
16 wess ⊢ ( ran 𝐺 ⊆ ( 𝐵 × 𝐴 ) → ( 𝑄 We ( 𝐵 × 𝐴 ) → 𝑄 We ran 𝐺 ) )
17 13 15 16 sylc ⊢ ( 𝜑 → 𝑄 We ran 𝐺 )
18 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
19 id ⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
20 18 19 opeq12d ⊢ ( 𝑧 = 𝑥 → ⟨ ( 𝐹 ‘ 𝑧 ) , 𝑧 ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ )
21 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ ∈ V
22 20 7 21 fvmpt ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐺 ‘ 𝑥 ) = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ )
23 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
24 id ⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
25 23 24 opeq12d ⊢ ( 𝑧 = 𝑦 → ⟨ ( 𝐹 ‘ 𝑧 ) , 𝑧 ⟩ = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ )
26 opex ⊢ ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ∈ V
27 25 7 26 fvmpt ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐺 ‘ 𝑦 ) = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ )
28 22 27 eqeqan12d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ) )
29 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
30 vex ⊢ 𝑥 ∈ V
31 29 30 opth ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 = 𝑦 ) )
32 31 simprbi ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 )
33 28 32 biimtrdi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
34 33 rgen2 ⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 )
35 dff13 ⊢ ( 𝐺 : 𝐴 –1-1→ ( 𝐵 × 𝐴 ) ↔ ( 𝐺 : 𝐴 ⟶ ( 𝐵 × 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
36 11 34 35 sylanblrc ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐺 : 𝐴 –1-1→ ( 𝐵 × 𝐴 ) )
37 f1f1orn ⊢ ( 𝐺 : 𝐴 –1-1→ ( 𝐵 × 𝐴 ) → 𝐺 : 𝐴 –1-1-onto→ ran 𝐺 )
38 f1ocnv ⊢ ( 𝐺 : 𝐴 –1-1-onto→ ran 𝐺 → ◡ 𝐺 : ran 𝐺 –1-1-onto→ 𝐴 )
39 2 36 37 38 4syl ⊢ ( 𝜑 → ◡ 𝐺 : ran 𝐺 –1-1-onto→ 𝐴 )
40 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) }
41 40 f1oiso2 ⊢ ( ◡ 𝐺 : ran 𝐺 –1-1-onto→ 𝐴 → ◡ 𝐺 Isom 𝑄 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) } ( ran 𝐺 , 𝐴 ) )
42 frel ⊢ ( 𝐺 : 𝐴 ⟶ ( 𝐵 × 𝐴 ) → Rel 𝐺 )
43 dfrel2 ⊢ ( Rel 𝐺 ↔ ◡ ◡ 𝐺 = 𝐺 )
44 42 43 sylib ⊢ ( 𝐺 : 𝐴 ⟶ ( 𝐵 × 𝐴 ) → ◡ ◡ 𝐺 = 𝐺 )
45 44 fveq1d ⊢ ( 𝐺 : 𝐴 ⟶ ( 𝐵 × 𝐴 ) → ( ◡ ◡ 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
46 44 fveq1d ⊢ ( 𝐺 : 𝐴 ⟶ ( 𝐵 × 𝐴 ) → ( ◡ ◡ 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
47 45 46 breq12d ⊢ ( 𝐺 : 𝐴 ⟶ ( 𝐵 × 𝐴 ) → ( ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑥 ) 𝑄 ( 𝐺 ‘ 𝑦 ) ) )
48 11 47 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑥 ) 𝑄 ( 𝐺 ‘ 𝑦 ) ) )
49 48 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑥 ) 𝑄 ( 𝐺 ‘ 𝑦 ) ) )
50 22 27 breqan12d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) 𝑄 ( 𝐺 ‘ 𝑦 ) ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ 𝑄 ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ) )
51 50 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ 𝑥 ) 𝑄 ( 𝐺 ‘ 𝑦 ) ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ 𝑄 ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ) )
52 eleq1 ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( 𝑢 ∈ ( 𝐵 × 𝐴 ) ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( 𝐵 × 𝐴 ) ) )
53 opelxp ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( 𝐵 × 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
54 52 53 bitrdi ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( 𝑢 ∈ ( 𝐵 × 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) )
55 54 anbi1d ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( ( 𝑢 ∈ ( 𝐵 × 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ↔ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ) )
56 29 30 op1std ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( 1st ‘ 𝑢 ) = ( 𝐹 ‘ 𝑥 ) )
57 56 breq1d ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( ( 1st ‘ 𝑢 ) 𝑅 ( 1st ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑣 ) ) )
58 56 eqeq1d ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑣 ) ) )
59 29 30 op2ndd ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( 2nd ‘ 𝑢 ) = 𝑥 )
60 59 breq1d ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( ( 2nd ‘ 𝑢 ) 𝑆 ( 2nd ‘ 𝑣 ) ↔ 𝑥 𝑆 ( 2nd ‘ 𝑣 ) ) )
61 58 60 anbi12d ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑣 ) ∧ ( 2nd ‘ 𝑢 ) 𝑆 ( 2nd ‘ 𝑣 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑣 ) ∧ 𝑥 𝑆 ( 2nd ‘ 𝑣 ) ) ) )
62 57 61 orbi12d ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( ( ( 1st ‘ 𝑢 ) 𝑅 ( 1st ‘ 𝑣 ) ∨ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑣 ) ∧ ( 2nd ‘ 𝑢 ) 𝑆 ( 2nd ‘ 𝑣 ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑣 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑣 ) ∧ 𝑥 𝑆 ( 2nd ‘ 𝑣 ) ) ) ) )
63 55 62 anbi12d ⊢ ( 𝑢 = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ → ( ( ( 𝑢 ∈ ( 𝐵 × 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ∧ ( ( 1st ‘ 𝑢 ) 𝑅 ( 1st ‘ 𝑣 ) ∨ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑣 ) ∧ ( 2nd ‘ 𝑢 ) 𝑆 ( 2nd ‘ 𝑣 ) ) ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑣 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑣 ) ∧ 𝑥 𝑆 ( 2nd ‘ 𝑣 ) ) ) ) ) )
64 eleq1 ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( 𝑣 ∈ ( 𝐵 × 𝐴 ) ↔ ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ∈ ( 𝐵 × 𝐴 ) ) )
65 opelxp ⊢ ( ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ∈ ( 𝐵 × 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) )
66 64 65 bitrdi ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( 𝑣 ∈ ( 𝐵 × 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) )
67 66 anbi2d ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ↔ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) ) )
68 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
69 vex ⊢ 𝑦 ∈ V
70 68 69 op1std ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( 1st ‘ 𝑣 ) = ( 𝐹 ‘ 𝑦 ) )
71 70 breq2d ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ) )
72 70 eqeq2d ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
73 68 69 op2ndd ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( 2nd ‘ 𝑣 ) = 𝑦 )
74 73 breq2d ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( 𝑥 𝑆 ( 2nd ‘ 𝑣 ) ↔ 𝑥 𝑆 𝑦 ) )
75 72 74 anbi12d ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑣 ) ∧ 𝑥 𝑆 ( 2nd ‘ 𝑣 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) )
76 71 75 orbi12d ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑣 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑣 ) ∧ 𝑥 𝑆 ( 2nd ‘ 𝑣 ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) )
77 67 76 anbi12d ⊢ ( 𝑣 = ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ → ( ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑣 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑣 ) ∧ 𝑥 𝑆 ( 2nd ‘ 𝑣 ) ) ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) ) )
78 21 26 63 77 6 brab ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ 𝑄 ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ↔ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) )
79 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
80 simpr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
81 79 80 jca ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
82 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
83 simpr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
84 82 83 jca ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) )
85 81 84 anim12dan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) )
86 85 biantrurd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) ) )
87 78 86 bitr4id ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ 𝑄 ⟨ ( 𝐹 ‘ 𝑦 ) , 𝑦 ⟩ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) )
88 49 51 87 3bitrrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ↔ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) )
89 88 pm5.32da ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) ) )
90 89 opabbidv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) } )
91 1 90 eqtrid ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) } )
92 isoeq3 ⊢ ( 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) } → ( ◡ 𝐺 Isom 𝑄 , 𝑇 ( ran 𝐺 , 𝐴 ) ↔ ◡ 𝐺 Isom 𝑄 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) } ( ran 𝐺 , 𝐴 ) ) )
93 91 92 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐺 Isom 𝑄 , 𝑇 ( ran 𝐺 , 𝐴 ) ↔ ◡ 𝐺 Isom 𝑄 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ◡ ◡ 𝐺 ‘ 𝑥 ) 𝑄 ( ◡ ◡ 𝐺 ‘ 𝑦 ) ) } ( ran 𝐺 , 𝐴 ) ) )
94 41 93 imbitrrid ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐺 : ran 𝐺 –1-1-onto→ 𝐴 → ◡ 𝐺 Isom 𝑄 , 𝑇 ( ran 𝐺 , 𝐴 ) ) )
95 2 39 94 sylc ⊢ ( 𝜑 → ◡ 𝐺 Isom 𝑄 , 𝑇 ( ran 𝐺 , 𝐴 ) )
96 isocnv ⊢ ( ◡ 𝐺 Isom 𝑄 , 𝑇 ( ran 𝐺 , 𝐴 ) → ◡ ◡ 𝐺 Isom 𝑇 , 𝑄 ( 𝐴 , ran 𝐺 ) )
97 95 96 syl ⊢ ( 𝜑 → ◡ ◡ 𝐺 Isom 𝑇 , 𝑄 ( 𝐴 , ran 𝐺 ) )
98 imacnvcnv ⊢ ( ◡ ◡ 𝐺 “ 𝑤 ) = ( 𝐺 “ 𝑤 )
99 vex ⊢ 𝑤 ∈ V
100 xpexg ⊢ ( ( ( 𝐹 “ 𝑤 ) ∈ V ∧ 𝑤 ∈ V ) → ( ( 𝐹 “ 𝑤 ) × 𝑤 ) ∈ V )
101 5 99 100 sylancl ⊢ ( 𝜑 → ( ( 𝐹 “ 𝑤 ) × 𝑤 ) ∈ V )
102 imadmres ⊢ ( 𝐺 “ dom ( 𝐺 ↾ 𝑤 ) ) = ( 𝐺 “ 𝑤 )
103 dmres ⊢ dom ( 𝐺 ↾ 𝑤 ) = ( 𝑤 ∩ dom 𝐺 )
104 103 elin2 ⊢ ( 𝑥 ∈ dom ( 𝐺 ↾ 𝑤 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) )
105 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → 𝑥 ∈ dom 𝐺 )
106 f1dm ⊢ ( 𝐺 : 𝐴 –1-1→ ( 𝐵 × 𝐴 ) → dom 𝐺 = 𝐴 )
107 2 36 106 3syl ⊢ ( 𝜑 → dom 𝐺 = 𝐴 )
108 107 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → dom 𝐺 = 𝐴 )
109 105 108 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → 𝑥 ∈ 𝐴 )
110 109 22 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) = ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ )
111 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
112 111 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → 𝐹 Fn 𝐴 )
113 dmres ⊢ dom ( 𝐹 ↾ 𝑤 ) = ( 𝑤 ∩ dom 𝐹 )
114 inss2 ⊢ ( 𝑤 ∩ dom 𝐹 ) ⊆ dom 𝐹
115 112 fndmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → dom 𝐹 = 𝐴 )
116 114 115 sseqtrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → ( 𝑤 ∩ dom 𝐹 ) ⊆ 𝐴 )
117 113 116 eqsstrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → dom ( 𝐹 ↾ 𝑤 ) ⊆ 𝐴 )
118 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → 𝑥 ∈ 𝑤 )
119 109 115 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → 𝑥 ∈ dom 𝐹 )
120 113 elin2 ⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝑤 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐹 ) )
121 118 119 120 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → 𝑥 ∈ dom ( 𝐹 ↾ 𝑤 ) )
122 fnfvima ⊢ ( ( 𝐹 Fn 𝐴 ∧ dom ( 𝐹 ↾ 𝑤 ) ⊆ 𝐴 ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝑤 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ dom ( 𝐹 ↾ 𝑤 ) ) )
123 112 117 121 122 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ dom ( 𝐹 ↾ 𝑤 ) ) )
124 imadmres ⊢ ( 𝐹 “ dom ( 𝐹 ↾ 𝑤 ) ) = ( 𝐹 “ 𝑤 )
125 123 124 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝑤 ) )
126 125 118 opelxpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → ⟨ ( 𝐹 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) )
127 110 126 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) )
128 104 127 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( 𝐺 ↾ 𝑤 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) )
129 128 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ dom ( 𝐺 ↾ 𝑤 ) ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) )
130 f1fun ⊢ ( 𝐺 : 𝐴 –1-1→ ( 𝐵 × 𝐴 ) → Fun 𝐺 )
131 2 36 130 3syl ⊢ ( 𝜑 → Fun 𝐺 )
132 resss ⊢ ( 𝐺 ↾ 𝑤 ) ⊆ 𝐺
133 dmss ⊢ ( ( 𝐺 ↾ 𝑤 ) ⊆ 𝐺 → dom ( 𝐺 ↾ 𝑤 ) ⊆ dom 𝐺 )
134 132 133 ax-mp ⊢ dom ( 𝐺 ↾ 𝑤 ) ⊆ dom 𝐺
135 funimass4 ⊢ ( ( Fun 𝐺 ∧ dom ( 𝐺 ↾ 𝑤 ) ⊆ dom 𝐺 ) → ( ( 𝐺 “ dom ( 𝐺 ↾ 𝑤 ) ) ⊆ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) ↔ ∀ 𝑥 ∈ dom ( 𝐺 ↾ 𝑤 ) ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) ) )
136 131 134 135 sylancl ⊢ ( 𝜑 → ( ( 𝐺 “ dom ( 𝐺 ↾ 𝑤 ) ) ⊆ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) ↔ ∀ 𝑥 ∈ dom ( 𝐺 ↾ 𝑤 ) ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) ) )
137 129 136 mpbird ⊢ ( 𝜑 → ( 𝐺 “ dom ( 𝐺 ↾ 𝑤 ) ) ⊆ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) )
138 102 137 eqsstrrid ⊢ ( 𝜑 → ( 𝐺 “ 𝑤 ) ⊆ ( ( 𝐹 “ 𝑤 ) × 𝑤 ) )
139 101 138 ssexd ⊢ ( 𝜑 → ( 𝐺 “ 𝑤 ) ∈ V )
140 98 139 eqeltrid ⊢ ( 𝜑 → ( ◡ ◡ 𝐺 “ 𝑤 ) ∈ V )
141 140 alrimiv ⊢ ( 𝜑 → ∀ 𝑤 ( ◡ ◡ 𝐺 “ 𝑤 ) ∈ V )
142 isowe2 ⊢ ( ( ◡ ◡ 𝐺 Isom 𝑇 , 𝑄 ( 𝐴 , ran 𝐺 ) ∧ ∀ 𝑤 ( ◡ ◡ 𝐺 “ 𝑤 ) ∈ V ) → ( 𝑄 We ran 𝐺 → 𝑇 We 𝐴 ) )
143 97 141 142 syl2anc ⊢ ( 𝜑 → ( 𝑄 We ran 𝐺 → 𝑇 We 𝐴 ) )
144 17 143 mpd ⊢ ( 𝜑 → 𝑇 We 𝐴 )