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

Metamath Proof Explorer

Theorem oemapvali

Description: If F < G , then there is some z witnessing this, but we can say more and in fact there is a definable expression X that also witnesses F < G . (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
oemapval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
oemapval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
oemapvali.r ⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
oemapvali.x ⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
Assertion oemapvali ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5 oemapval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
6 oemapval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
7 oemapvali.r ⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
8 oemapvali.x ⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
9 1 2 3 4 5 6 oemapval ⊢ ( 𝜑 → ( 𝐹 𝑇 𝐺 ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) )
10 7 9 mpbid ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
11 ssrab2 ⊢ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ 𝐵
12 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝐵 ∈ On )
13 onss ⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
14 12 13 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝐵 ⊆ On )
15 11 14 sstrid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ On )
16 1 2 3 cantnfs ⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
17 6 16 mpbid ⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
18 17 simprd ⊢ ( 𝜑 → 𝐺 finSupp ∅ )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝐺 finSupp ∅ )
20 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) ) → 𝐵 ∈ On )
21 simp2 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) ) → 𝑐 ∈ 𝐵 )
22 17 simpld ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
23 22 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
24 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) ) → 𝐺 Fn 𝐵 )
25 ne0i ⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) → ( 𝐺 ‘ 𝑐 ) ≠ ∅ )
26 25 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) ) → ( 𝐺 ‘ 𝑐 ) ≠ ∅ )
27 fvn0elsupp ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑐 ) ≠ ∅ ) ) → 𝑐 ∈ ( 𝐺 supp ∅ ) )
28 20 21 24 26 27 syl22anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) ) → 𝑐 ∈ ( 𝐺 supp ∅ ) )
29 28 rabssdv ⊢ ( 𝜑 → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ ( 𝐺 supp ∅ ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ ( 𝐺 supp ∅ ) )
31 fsuppimp ⊢ ( 𝐺 finSupp ∅ → ( Fun 𝐺 ∧ ( 𝐺 supp ∅ ) ∈ Fin ) )
32 ssfi ⊢ ( ( ( 𝐺 supp ∅ ) ∈ Fin ∧ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ ( 𝐺 supp ∅ ) ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ Fin )
33 32 ex ⊢ ( ( 𝐺 supp ∅ ) ∈ Fin → ( { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ ( 𝐺 supp ∅ ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ Fin ) )
34 31 33 simpl2im ⊢ ( 𝐺 finSupp ∅ → ( { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ ( 𝐺 supp ∅ ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ Fin ) )
35 19 30 34 sylc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ Fin )
36 fveq2 ⊢ ( 𝑐 = 𝑧 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑧 ) )
37 fveq2 ⊢ ( 𝑐 = 𝑧 → ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ 𝑧 ) )
38 36 37 eleq12d ⊢ ( 𝑐 = 𝑧 → ( ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ) )
39 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑧 ∈ 𝐵 )
40 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) )
41 38 39 40 elrabd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑧 ∈ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } )
42 41 ne0d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ≠ ∅ )
43 ordunifi ⊢ ( ( { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ On ∧ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ Fin ∧ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ≠ ∅ ) → ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } )
44 15 35 42 43 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } )
45 8 44 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑋 ∈ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } )
46 11 45 sselid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑋 ∈ 𝐵 )
47 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
48 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
49 47 48 eleq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ) )
50 fveq2 ⊢ ( 𝑐 = 𝑥 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑥 ) )
51 fveq2 ⊢ ( 𝑐 = 𝑥 → ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ 𝑥 ) )
52 50 51 eleq12d ⊢ ( 𝑐 = 𝑥 → ( ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑥 ) ) )
53 52 cbvrabv ⊢ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑥 ) }
54 49 53 elrab2 ⊢ ( 𝑋 ∈ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ) )
55 45 54 sylib ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ) )
56 55 simprd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) )
57 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
58 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝐴 ∈ On )
59 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝐺 : 𝐵 ⟶ 𝐴 )
60 59 46 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
61 onelon ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑋 ) ∈ On )
62 58 60 61 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝐺 ‘ 𝑋 ) ∈ On )
63 eloni ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ On → Ord ( 𝐺 ‘ 𝑋 ) )
64 ordirr ⊢ ( Ord ( 𝐺 ‘ 𝑋 ) → ¬ ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) )
65 62 63 64 3syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ¬ ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) )
66 nelneq ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ¬ ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ) → ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
67 56 65 66 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
68 eleq2 ⊢ ( 𝑤 = 𝑋 → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑋 ) )
69 fveq2 ⊢ ( 𝑤 = 𝑋 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑋 ) )
70 fveq2 ⊢ ( 𝑤 = 𝑋 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑋 ) )
71 69 70 eqeq12d ⊢ ( 𝑤 = 𝑋 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) ) )
72 68 71 imbi12d ⊢ ( 𝑤 = 𝑋 → ( ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ↔ ( 𝑧 ∈ 𝑋 → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) ) ) )
73 72 57 46 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝑧 ∈ 𝑋 → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) ) )
74 67 73 mtod ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ¬ 𝑧 ∈ 𝑋 )
75 ssexg ⊢ ( ( { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ 𝐵 ∧ 𝐵 ∈ On ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ V )
76 11 12 75 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ V )
77 ssonuni ⊢ ( { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ V → ( { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ⊆ On → ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ On ) )
78 76 15 77 sylc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } ∈ On )
79 8 78 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑋 ∈ On )
80 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ On )
81 12 39 80 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑧 ∈ On )
82 ontri1 ⊢ ( ( 𝑋 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑋 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑋 ) )
83 79 81 82 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝑋 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑋 ) )
84 74 83 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑋 ⊆ 𝑧 )
85 elssuni ⊢ ( 𝑧 ∈ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } → 𝑧 ⊆ ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } )
86 85 8 sseqtrrdi ⊢ ( 𝑧 ∈ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) } → 𝑧 ⊆ 𝑋 )
87 41 86 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑧 ⊆ 𝑋 )
88 84 87 eqssd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → 𝑋 = 𝑧 )
89 eleq1 ⊢ ( 𝑋 = 𝑧 → ( 𝑋 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤 ) )
90 89 imbi1d ⊢ ( 𝑋 = 𝑧 → ( ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ↔ ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
91 90 ralbidv ⊢ ( 𝑋 = 𝑧 → ( ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
92 88 91 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
93 57 92 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
94 46 56 93 3jca ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
95 10 94 rexlimddv ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )