Theorem cantnflem1c

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019) (Proof shortened by AV, 4-Apr-2020)

	Ref	Expression
Hypotheses	cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
	cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
	oemapval.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
	oemapval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
	oemapval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
	oemapvali.r	⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
	oemapvali.x	⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
	cantnflem1.o	⊢ 𝑂 = OrdIso ( E , ( 𝐺 supp ∅ ) )
Assertion	cantnflem1c	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑥 ∈ ( 𝐺 supp ∅ ) )

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		cantnflem1.o	⊢ 𝑂 = OrdIso ( E , ( 𝐺 supp ∅ ) )
10	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝐵 ∈ On )
11		simplr	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑥 ∈ 𝐵 )
12	1 2 3	cantnfs	⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
13	6 12	mpbid	⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
14	13	simpld	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
15	14	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
16	15	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝐺 Fn 𝐵 )
17	1 2 3 4 5 6 7 8 9	cantnflem1b	⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑋 ⊆ ( 𝑂 ‘ 𝑢 ) )
18	17	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑋 ⊆ ( 𝑂 ‘ 𝑢 ) )
19		simprr	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 )
20	1 2 3 4 5 6 7 8	oemapvali	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
21	20	simp1d	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
22		onelon	⊢ ( ( 𝐵 ∈ On ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ On )
23	3 21 22	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ On )
24	23	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑋 ∈ On )
25		onss	⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
26	3 25	syl	⊢ ( 𝜑 → 𝐵 ⊆ On )
27	26	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
28	27	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑥 ∈ On )
29		ontr2	⊢ ( ( 𝑋 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑋 ⊆ ( 𝑂 ‘ 𝑢 ) ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) → 𝑋 ∈ 𝑥 ) )
30	24 28 29	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( ( 𝑋 ⊆ ( 𝑂 ‘ 𝑢 ) ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) → 𝑋 ∈ 𝑥 ) )
31	18 19 30	mp2and	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑋 ∈ 𝑥 )
32		eleq2w	⊢ ( 𝑤 = 𝑥 → ( 𝑋 ∈ 𝑤 ↔ 𝑋 ∈ 𝑥 ) )
33		fveq2	⊢ ( 𝑤 = 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑥 ) )
34		fveq2	⊢ ( 𝑤 = 𝑥 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑥 ) )
35	33 34	eqeq12d	⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
36	32 35	imbi12d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ↔ ( 𝑋 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
37	20	simp3d	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
38	37	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
39	36 38 11	rspcdva	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝑋 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
40	31 39	mpd	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
41		simprl	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
42	40 41	eqnetrrd	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ≠ ∅ )
43		fvn0elsupp	⊢ ( ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺 ‘ 𝑥 ) ≠ ∅ ) ) → 𝑥 ∈ ( 𝐺 supp ∅ ) )
44	10 11 16 42 43	syl22anc	⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑥 ∈ ( 𝐺 supp ∅ ) )