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	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐺 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) ) ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
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	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )