Theorem pwfseqlem4 10674

Description: Lemma for pwfseq 10676. Derive a final contradiction from the function 𝐹 in pwfseqlem3 10672. Applying fpwwe2 10655 to it, we get a certain maximal well-ordered subset 𝑍, but the defining property (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 contradicts our assumption on 𝐹, so we are reduced to the case of 𝑍 finite. This too is a contradiction, though, because 𝑍 and its preimage under (𝑊‘𝑍) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by Matthew House, 10-Sep-2025.)

Hypotheses

Ref	Expression
pwfseqlem4.g	⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))
pwfseqlem4.x	⊢ (𝜑 → 𝑋 ⊆ 𝐴)
pwfseqlem4.h	⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)
pwfseqlem4.ps	⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))
pwfseqlem4.k	⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥)
pwfseqlem4.d	⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))})
pwfseqlem4.f	⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))
pwfseqlem4.w	⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))}
pwfseqlem4.z	⊢ 𝑍 = ∪ dom 𝑊

Assertion

Ref	Expression
pwfseqlem4	⊢ ¬ 𝜑

Distinct variable groups:   𝑛,𝑟,𝑤,𝑥,𝑧   𝐷,𝑛,𝑧   𝑎,𝑏,𝑠,𝑣,𝐹   𝑤,𝐺   𝑤,𝐾   𝑟,𝑎,𝑥,𝑧,𝐻,𝑏,𝑠,𝑣   𝑛,𝑎,𝜑,𝑏,𝑠,𝑣,𝑟,𝑥,𝑧   𝜓,𝑛,𝑧   𝐴,𝑎,𝑛,𝑟,𝑠,𝑥,𝑧   𝑊,𝑎,𝑏,𝑠,𝑣   𝑍,𝑎,𝑏,𝑠,𝑣

Allowed substitution hints:   𝜑(𝑤)   𝜓(𝑥, 𝑤, 𝑣, 𝑠, 𝑟, 𝑎, 𝑏)   𝐴(𝑤, 𝑣, 𝑏)   𝐷(𝑥, 𝑤, 𝑣, 𝑠, 𝑟, 𝑎, 𝑏)   𝐹(𝑥, 𝑧, 𝑤, 𝑛, 𝑟)   𝐺(𝑥, 𝑧, 𝑣, 𝑛, 𝑠, 𝑟, 𝑎, 𝑏)   𝐻(𝑤, 𝑛)   𝐾(𝑥, 𝑧, 𝑣, 𝑛, 𝑠, 𝑟, 𝑎, 𝑏)   𝑊(𝑥, 𝑧, 𝑤, 𝑛, 𝑟)   𝑋(𝑥, 𝑧, 𝑤, 𝑣, 𝑛, 𝑠, 𝑟, 𝑎, 𝑏)   𝑍(𝑥, 𝑧, 𝑤, 𝑛, 𝑟)

Proof of Theorem pwfseqlem4

Step	Hyp	Ref	Expression
1		eqid 2762	. . . . . . . . . . . . 13 ⊢ 𝑍 = 𝑍
2		eqid 2762	. . . . . . . . . . . . 13 ⊢ (𝑊‘𝑍) = (𝑊‘𝑍)
3	1, 2	pm3.2i 476	. . . . . . . . . . . 12 ⊢ (𝑍 = 𝑍 ∧ (𝑊‘𝑍) = (𝑊‘𝑍))
4		pwfseqlem4.w	. . . . . . . . . . . . 13 ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))}
5		pwfseqlem4.g	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))
6		omex 9625	. . . . . . . . . . . . . . . 16 ⊢ ω ∈ V
7		ovex 7449	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ↑m 𝑛) ∈ V
8	6, 7	iunex 7968	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∈ V
9		f1dmex 7957	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
10	5, 8, 9	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
11		pwexb 7768	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
12	10, 11	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ V)
13		pwfseqlem4.x	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
14		pwfseqlem4.h	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)
15		pwfseqlem4.ps	. . . . . . . . . . . . . 14 ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))
16		pwfseqlem4.k	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥)
17		pwfseqlem4.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))})
18		pwfseqlem4.f	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))
19	5, 13, 14, 15, 16, 17, 18	pwfseqlem4a 10673	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴)
20		pwfseqlem4.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = ∪ dom 𝑊
21	4, 12, 19, 20	fpwwe2 10655	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑍𝑊(𝑊‘𝑍) ∧ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍) ↔ (𝑍 = 𝑍 ∧ (𝑊‘𝑍) = (𝑊‘𝑍))))
22	3, 21	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍𝑊(𝑊‘𝑍) ∧ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍))
23	22	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍𝑊(𝑊‘𝑍))
24	4, 12	fpwwe2lem2 10644	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍𝑊(𝑊‘𝑍) ↔ ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏))))
25	23, 24	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)))
26		id 23	. . . . . . . . . . 11 ⊢ ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))
27	26	3expa 1136	. . . . . . . . . 10 ⊢ (((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ (𝑊‘𝑍) We 𝑍) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))
28	27	adantrr 730	. . . . . . . . 9 ⊢ (((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))
29	25, 28	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))
30	22	simprd 501	. . . . . . . 8 ⊢ (𝜑 → (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍)
31	25	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)))
32	31	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ 𝐴)
33	12, 32	ssexd 5293	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ V)
34		fvexd 6897	. . . . . . . . 9 ⊢ (𝜑 → (𝑊‘𝑍) ∈ V)
35		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → 𝑎 = 𝑍)
36	35	sseq1d 3965	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑎 ⊆ 𝐴 ↔ 𝑍 ⊆ 𝐴))
37		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → 𝑠 = (𝑊‘𝑍))
38	35	sqxpeqd 5691	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑎 × 𝑎) = (𝑍 × 𝑍))
39	37, 38	sseq12d 3967	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑠 ⊆ (𝑎 × 𝑎) ↔ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)))
40	37, 35	weeq12d 5648	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑠 We 𝑎 ↔ (𝑊‘𝑍) We 𝑍))
41	36, 39, 40	3anbi123d 1464	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ↔ (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍)))
42		oveq12 7425	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑎𝐹𝑠) = (𝑍𝐹(𝑊‘𝑍)))
43	42, 35	eleq12d 2856	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → ((𝑎𝐹𝑠) ∈ 𝑎 ↔ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍))
44	35	breq1d 5117	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (𝑎 ≺ ω ↔ 𝑍 ≺ ω))
45	43, 44	imbi12d 347	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω) ↔ ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω)))
46	41, 45	imbi12d 347	. . . . . . . . 9 ⊢ ((𝑎 = 𝑍 ∧ 𝑠 = (𝑊‘𝑍)) → (((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) → ((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω)) ↔ ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍) → ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω))))
47		omelon 9628	. . . . . . . . . . . . . 14 ⊢ ω ∈ On
48		onenon 9957	. . . . . . . . . . . . . 14 ⊢ (ω ∈ On → ω ∈ dom card)
49	47, 48	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ω ∈ dom card
50		simpr3 1215	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑠 We 𝑎)
51	50	19.8ad 2220	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ∃𝑠 𝑠 We 𝑎)
52		ween 10041	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom card ↔ ∃𝑠 𝑠 We 𝑎)
53	51, 52	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑎 ∈ dom card)
54		domtri2 9997	. . . . . . . . . . . . 13 ⊢ ((ω ∈ dom card ∧ 𝑎 ∈ dom card) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω))
55	49, 53, 54	sylancr 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω))
56		nfv 1947	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))
57		nfcv 2924	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟𝑎
58		nfmpo2 7497	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))
59	18, 58	nfcxfr 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟𝐹
60		nfcv 2924	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟𝑠
61	57, 59, 60	nfov 7446	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟(𝑎𝐹𝑠)
62	61	nfel1 2940	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟(𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)
63	56, 62	nfim 1929	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑟((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))
64		sseq1 3959	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑠 → (𝑟 ⊆ (𝑎 × 𝑎) ↔ 𝑠 ⊆ (𝑎 × 𝑎)))
65		weeq1 5646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑠 → (𝑟 We 𝑎 ↔ 𝑠 We 𝑎))
66	64, 65	3anbi23d 1467	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑠 → ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)))
67	66	anbi1d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑠 → (((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)))
68	67	anbi2d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑠 → ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))))
69		oveq2 7424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑠 → (𝑎𝐹𝑟) = (𝑎𝐹𝑠))
70	69	eleq1d 2847	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑠 → ((𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎) ↔ (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)))
71	68, 70	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑠 → (((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))))
72		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))
73		nfcv 2924	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝑎
74		nfmpo1 7496	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))
75	18, 74	nfcxfr 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐹
76		nfcv 2924	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝑟
77	73, 75, 76	nfov 7446	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝑎𝐹𝑟)
78	77	nfel1 2940	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)
79	72, 78	nfim 1929	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))
80		sseq1 3959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴))
81		xpeq12 5684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 = 𝑎 ∧ 𝑥 = 𝑎) → (𝑥 × 𝑥) = (𝑎 × 𝑎))
82	81	anidms 577	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 → (𝑥 × 𝑥) = (𝑎 × 𝑎))
83	82	sseq2d 3966	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑟 ⊆ (𝑎 × 𝑎)))
84		weeq2 5647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑎))
85	80, 83, 84	3anbi123d 1464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑎 → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎)))
86		breq2 5111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑎 → (ω ≼ 𝑥 ↔ ω ≼ 𝑎))
87	85, 86	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑎 → (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))
88	15, 87	bitrid 286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑎 → (𝜓 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))
89	88	anbi2d 642	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))))
90		oveq1 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑎 → (𝑥𝐹𝑟) = (𝑎𝐹𝑟))
91		difeq2 4071	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑎 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑎))
92	90, 91	eleq12d 2856	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑎 → ((𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥) ↔ (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)))
93	89, 92	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))))
94	5, 13, 14, 15, 16, 17, 18	pwfseqlem3 10672	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥))
95	79, 93, 94	chvarfv 2278	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))
96	63, 71, 95	chvarfv 2278	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))
97	96	eldifbd 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → ¬ (𝑎𝐹𝑠) ∈ 𝑎)
98	97	expr 462	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 → ¬ (𝑎𝐹𝑠) ∈ 𝑎))
99	55, 98	sylbird 263	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (¬ 𝑎 ≺ ω → ¬ (𝑎𝐹𝑠) ∈ 𝑎))
100	99	con4d 116	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω))
101	100	ex 418	. . . . . . . . 9 ⊢ (𝜑 → ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) → ((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω)))
102	33, 34, 46, 101	vtocl2d 3526	. . . . . . . 8 ⊢ (𝜑 → ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍) → ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω)))
103	29, 30, 102	mp2d 50	. . . . . . 7 ⊢ (𝜑 → 𝑍 ≺ ω)
104		isfinite 9634	. . . . . . 7 ⊢ (𝑍 ∈ Fin ↔ 𝑍 ≺ ω)
105	103, 104	sylibr 237	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ Fin)
106		fvex 6895	. . . . . 6 ⊢ (𝑊‘𝑍) ∈ V
107	5, 13, 14, 15, 16, 17, 18	pwfseqlem2 10671	. . . . . 6 ⊢ ((𝑍 ∈ Fin ∧ (𝑊‘𝑍) ∈ V) → (𝑍𝐹(𝑊‘𝑍)) = (𝐻‘(card‘𝑍)))
108	105, 106, 107	sylancl 598	. . . . 5 ⊢ (𝜑 → (𝑍𝐹(𝑊‘𝑍)) = (𝐻‘(card‘𝑍)))
109	108, 30	eqeltrrd 2863	. . . 4 ⊢ (𝜑 → (𝐻‘(card‘𝑍)) ∈ 𝑍)
110	4, 12, 23	fpwwe2lem3 10645	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐻‘(card‘𝑍)) ∈ 𝑍) → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘𝑍)))
111	109, 110	mpdan 700	. . . . . . . . 9 ⊢ (𝜑 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘𝑍)))
112		cnvimass 6082	. . . . . . . . . . . 12 ⊢ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ dom (𝑊‘𝑍)
113	31	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊‘𝑍) ⊆ (𝑍 × 𝑍))
114		dmss 5890	. . . . . . . . . . . . . 14 ⊢ ((𝑊‘𝑍) ⊆ (𝑍 × 𝑍) → dom (𝑊‘𝑍) ⊆ dom (𝑍 × 𝑍))
115	113, 114	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑊‘𝑍) ⊆ dom (𝑍 × 𝑍))
116		dmxpss 6168	. . . . . . . . . . . . 13 ⊢ dom (𝑍 × 𝑍) ⊆ 𝑍
117	115, 116	sstrdi 3946	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (𝑊‘𝑍) ⊆ 𝑍)
118	112, 117	sstrid 3945	. . . . . . . . . . 11 ⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍)
119	105, 118	ssfid 9242	. . . . . . . . . 10 ⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin)
120	106	inex1 5284	. . . . . . . . . 10 ⊢ ((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ∈ V
121	5, 13, 14, 15, 16, 17, 18	pwfseqlem2 10671	. . . . . . . . . 10 ⊢ (((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin ∧ ((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ∈ V) → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
122	119, 120, 121	sylancl 598	. . . . . . . . 9 ⊢ (𝜑 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
123	111, 122	eqtr3d 2799	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(card‘𝑍)) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
124		f1of1 6820	. . . . . . . . . 10 ⊢ (𝐻:ω–1-1-onto→𝑋 → 𝐻:ω–1-1→𝑋)
125	14, 124	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:ω–1-1→𝑋)
126		ficardom 9969	. . . . . . . . . 10 ⊢ (𝑍 ∈ Fin → (card‘𝑍) ∈ ω)
127	105, 126	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (card‘𝑍) ∈ ω)
128		ficardom 9969	. . . . . . . . . 10 ⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin → (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)
129	119, 128	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)
130		f1fveq 7262	. . . . . . . . 9 ⊢ ((𝐻:ω–1-1→𝑋 ∧ ((card‘𝑍) ∈ ω ∧ (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)) → ((𝐻‘(card‘𝑍)) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ↔ (card‘𝑍) = (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
131	125, 127, 129, 130	syl12anc 850	. . . . . . . 8 ⊢ (𝜑 → ((𝐻‘(card‘𝑍)) = (𝐻‘(card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ↔ (card‘𝑍) = (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
132	123, 131	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (card‘𝑍) = (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))
133	132	eqcomd 2768	. . . . . 6 ⊢ (𝜑 → (card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍))
134		finnum 9956	. . . . . . . 8 ⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card)
135	119, 134	syl 18	. . . . . . 7 ⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card)
136		finnum 9956	. . . . . . . 8 ⊢ (𝑍 ∈ Fin → 𝑍 ∈ dom card)
137	105, 136	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ dom card)
138		carden2 9995	. . . . . . 7 ⊢ (((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card ∧ 𝑍 ∈ dom card) → ((card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍) ↔ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
139	135, 137, 138	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((card‘(◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍) ↔ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
140	133, 139	mpbid 235	. . . . 5 ⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
141		dfpss2 4039	. . . . . . . 8 ⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍 ∧ ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
142	141	baib 545	. . . . . . 7 ⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
143	118, 142	syl 18	. . . . . 6 ⊢ (𝜑 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
144		php3 9206	. . . . . . . . 9 ⊢ ((𝑍 ∈ Fin ∧ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍) → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≺ 𝑍)
145		sdomnen 8990	. . . . . . . . 9 ⊢ ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≺ 𝑍 → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
146	144, 145	syl 18	. . . . . . . 8 ⊢ ((𝑍 ∈ Fin ∧ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍) → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
147	146	ex 418	. . . . . . 7 ⊢ (𝑍 ∈ Fin → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
148	105, 147	syl 18	. . . . . 6 ⊢ (𝜑 → ((◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
149	143, 148	sylbird 263	. . . . 5 ⊢ (𝜑 → (¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍 → ¬ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
150	140, 149	mt4d 118	. . . 4 ⊢ (𝜑 → (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍)
151	109, 150	eleqtrrd 2865	. . 3 ⊢ (𝜑 → (𝐻‘(card‘𝑍)) ∈ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))
152		fvex 6895	. . . 4 ⊢ (𝐻‘(card‘𝑍)) ∈ V
153	152	eliniseg 6094	. . . 4 ⊢ ((𝐻‘(card‘𝑍)) ∈ V → ((𝐻‘(card‘𝑍)) ∈ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ↔ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍))))
154	152, 153	ax-mp 5	. . 3 ⊢ ((𝐻‘(card‘𝑍)) ∈ (◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ↔ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))
155	151, 154	sylib 221	. 2 ⊢ (𝜑 → (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))
156	25	simprd 501	. . . . 5 ⊢ (𝜑 → ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏))
157	156	simpld 500	. . . 4 ⊢ (𝜑 → (𝑊‘𝑍) We 𝑍)
158		weso 5650	. . . 4 ⊢ ((𝑊‘𝑍) We 𝑍 → (𝑊‘𝑍) Or 𝑍)
159	157, 158	syl 18	. . 3 ⊢ (𝜑 → (𝑊‘𝑍) Or 𝑍)
160		sonr 5591	. . 3 ⊢ (((𝑊‘𝑍) Or 𝑍 ∧ (𝐻‘(card‘𝑍)) ∈ 𝑍) → ¬ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))
161	159, 109, 160	syl2anc 596	. 2 ⊢ (𝜑 → ¬ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))
162	155, 161	pm2.65i 196	1 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∀wral 3078  {crab 3414  Vcvv 3453  [wsbc 3742   ∖ cdif 3899   ∩ cin 3901   ⊆ wss 3902   ⊊ wpss 3903  ifcif 4485  𝒫 cpw 4560  {csn 4587  ∪ cuni 4870  ∩ cint 4910  ∪ ciun 4954   class class class wbr 5107  {copab 5171   Or wor 5566   We wwe 5611   × cxp 5657  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   “ cima 5662  Oncon0 6361  –1-1→wf1 6534  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7416   ∈ cmpo 7418  ωcom 7865   ↑_m cmap 8829   ≈ cen 8952   ≼ cdom 8953   ≺ csdm 8954  Fincfn 8955  cardccrd 9943

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-inf2 9623

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-er 8699  df-map 8831  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-oi 9485  df-card 9947

This theorem is used by:  pwfseqlem5  10675