pwfseqlem1

Description: Lemma for pwfseq . Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015)

	Ref	Expression
Hypotheses	pwfseqlem4.g	⊢ ( 𝜑 → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
	pwfseqlem4.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
	pwfseqlem4.h	⊢ ( 𝜑 → 𝐻 : ω –1-1-onto→ 𝑋 )
	pwfseqlem4.ps	⊢ ( 𝜓 ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) )
	pwfseqlem4.k	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) –1-1→ 𝑥 )
	pwfseqlem4.d	⊢ 𝐷 = ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } )
Assertion	pwfseqlem1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) ∖ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwfseqlem4.g	⊢ ( 𝜑 → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
2		pwfseqlem4.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
3		pwfseqlem4.h	⊢ ( 𝜑 → 𝐻 : ω –1-1-onto→ 𝑋 )
4		pwfseqlem4.ps	⊢ ( 𝜓 ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) )
5		pwfseqlem4.k	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) –1-1→ 𝑥 )
6		pwfseqlem4.d	⊢ 𝐷 = ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
8		f1f	⊢ ( 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) → 𝐺 : 𝒫 𝐴 ⟶ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
9	7 8	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : 𝒫 𝐴 ⟶ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
10		ssrab2	⊢ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ⊆ 𝑥
11		simprl1	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ∧ ω ≼ 𝑥 ) ) → 𝑥 ⊆ 𝐴 )
12	4 11	sylan2b	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ⊆ 𝐴 )
13	10 12	sstrid	⊢ ( ( 𝜑 ∧ 𝜓 ) → { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ⊆ 𝐴 )
14		vex	⊢ 𝑥 ∈ V
15	14	rabex	⊢ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ V
16	15	elpw	⊢ ( { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ 𝒫 𝐴 ↔ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ⊆ 𝐴 )
17	13 16	sylibr	⊢ ( ( 𝜑 ∧ 𝜓 ) → { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ 𝒫 𝐴 )
18	9 17	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
19	6 18	eqeltrid	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) )
20		pm5.19	⊢ ¬ ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } )
21	5	adantr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) –1-1→ 𝑥 )
22		f1f	⊢ ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) –1-1→ 𝑥 → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ⟶ 𝑥 )
23	21 22	syl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ⟶ 𝑥 )
24		ffvelcdm	⊢ ( ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ⟶ 𝑥 ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 )
25	23 24	sylancom	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 )
26		f1f1orn	⊢ ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) –1-1→ 𝑥 → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) –1-1-onto→ ran 𝐾 )
27	21 26	syl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) –1-1-onto→ ran 𝐾 )
28		f1ocnvfv1	⊢ ( ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) –1-1-onto→ ran 𝐾 ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) = 𝐷 )
29	27 28	sylancom	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) = 𝐷 )
30		f1fn	⊢ ( 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) → 𝐺 Fn 𝒫 𝐴 )
31	7 30	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 Fn 𝒫 𝐴 )
32		fnfvelrn	⊢ ( ( 𝐺 Fn 𝒫 𝐴 ∧ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ 𝒫 𝐴 ) → ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) ∈ ran 𝐺 )
33	31 17 32	syl2anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) ∈ ran 𝐺 )
34	6 33	eqeltrid	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ran 𝐺 )
35	34	adantr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → 𝐷 ∈ ran 𝐺 )
36	29 35	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 )
37		fveq2	⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ^◡ 𝐾 ‘ 𝑦 ) = ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) )
38	37	eleq1d	⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ( ^◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ↔ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ) )
39		id	⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → 𝑦 = ( 𝐾 ‘ 𝐷 ) )
40		2fveq3	⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) = ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) )
41	39 40	eleq12d	⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( 𝑦 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) ↔ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
42	41	notbid	⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ¬ 𝑦 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
43	38 42	anbi12d	⊢ ( 𝑦 = ( 𝐾 ‘ 𝐷 ) → ( ( ( ^◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ∧ ¬ 𝑦 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) ) ↔ ( ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) ) )
44		fveq2	⊢ ( 𝑤 = 𝑦 → ( ^◡ 𝐾 ‘ 𝑤 ) = ( ^◡ 𝐾 ‘ 𝑦 ) )
45	44	eleq1d	⊢ ( 𝑤 = 𝑦 → ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ↔ ( ^◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ) )
46		id	⊢ ( 𝑤 = 𝑦 → 𝑤 = 𝑦 )
47		2fveq3	⊢ ( 𝑤 = 𝑦 → ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) = ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) )
48	46 47	eleq12d	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ↔ 𝑦 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) ) )
49	48	notbid	⊢ ( 𝑤 = 𝑦 → ( ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ↔ ¬ 𝑦 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) ) )
50	45 49	anbi12d	⊢ ( 𝑤 = 𝑦 → ( ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) ↔ ( ( ^◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ∧ ¬ 𝑦 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) ) ) )
51	50	cbvrabv	⊢ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } = { 𝑦 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑦 ) ∈ ran 𝐺 ∧ ¬ 𝑦 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑦 ) ) ) }
52	43 51	elrab2	⊢ ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) ) )
53		anass	⊢ ( ( ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ) ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) ↔ ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) ) )
54	52 53	bitr4i	⊢ ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ( ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ) ∧ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
55	54	baib	⊢ ( ( ( 𝐾 ‘ 𝐷 ) ∈ 𝑥 ∧ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ∈ ran 𝐺 ) → ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
56	25 36 55	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ) )
57	29 6	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) = ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) )
58	57	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) = ( ^◡ 𝐺 ‘ ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) )
59		f1f1orn	⊢ ( 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) → 𝐺 : 𝒫 𝐴 –1-1-onto→ ran 𝐺 )
60	7 59	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : 𝒫 𝐴 –1-1-onto→ ran 𝐺 )
61		f1ocnvfv1	⊢ ( ( 𝐺 : 𝒫 𝐴 –1-1-onto→ ran 𝐺 ∧ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ∈ 𝒫 𝐴 ) → ( ^◡ 𝐺 ‘ ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) = { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } )
62	60 17 61	syl2anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ^◡ 𝐺 ‘ ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) = { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } )
63	62	adantr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ^◡ 𝐺 ‘ ( 𝐺 ‘ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) = { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } )
64	58 63	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) = { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } )
65	64	eleq2d	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ↔ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) )
66	65	notbid	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ¬ ( 𝐾 ‘ 𝐷 ) ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ ( 𝐾 ‘ 𝐷 ) ) ) ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) )
67	56 66	bitrd	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) → ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) )
68	67	ex	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) → ( ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ↔ ¬ ( 𝐾 ‘ 𝐷 ) ∈ { 𝑤 ∈ 𝑥 ∣ ( ( ^◡ 𝐾 ‘ 𝑤 ) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ ( ^◡ 𝐺 ‘ ( ^◡ 𝐾 ‘ 𝑤 ) ) ) } ) ) )
69	20 68	mtoi	⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ 𝐷 ∈ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) )
70	19 69	eldifd	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑_m 𝑛 ) ∖ ∪ 𝑛 ∈ ω ( 𝑥 ↑_m 𝑛 ) ) )

Metamath Proof Explorer

Theorem pwfseqlem1

Proof