pwfseqlem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pwfseqlem4		Structured version Visualization version GIF version

Theorem pwfseqlem4 10657

Description: Lemma for pwfseq 10659. Derive a final contradiction from the function 𝐹 in pwfseqlem3 10655. Applying fpwwe2 10638 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.)

**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 2733	. . . . . . . . . . 11 ⊢ 𝑍 = 𝑍
2		eqid 2733	. . . . . . . . . . 11 ⊢ (𝑊‘𝑍) = (𝑊‘𝑍)
3	1, 2	pm3.2i 472	. . . . . . . . . 10 ⊢ (𝑍 = 𝑍 ∧ (𝑊‘𝑍) = (𝑊‘𝑍))
4		pwfseqlem4.w	. . . . . . . . . . 11 ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(^◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))}
5		pwfseqlem4.g	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛))
6		omex 9638	. . . . . . . . . . . . . 14 ⊢ ω ∈ V
7		ovex 7442	. . . . . . . . . . . . . 14 ⊢ (𝐴 ↑_m 𝑛) ∈ V
8	6, 7	iunex 7955	. . . . . . . . . . . . 13 ⊢ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V
9		f1dmex 7943	. . . . . . . . . . . . 13 ⊢ ((𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑_m 𝑛) ∈ V) → 𝒫 𝐴 ∈ V)
10	5, 8, 9	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
11		pwexb 7753	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
12	10, 11	sylibr 233	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ V)
13		pwfseqlem4.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
14		pwfseqlem4.h	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)
15		pwfseqlem4.ps	. . . . . . . . . . . 12 ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))
16		pwfseqlem4.k	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑_m 𝑛)–1-1→𝑥)
17		pwfseqlem4.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((^◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (^◡𝐺‘(^◡𝐾‘𝑤)))})
18		pwfseqlem4.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))
19	5, 13, 14, 15, 16, 17, 18	pwfseqlem4a 10656	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴)
20		pwfseqlem4.z	. . . . . . . . . . 11 ⊢ 𝑍 = ∪ dom 𝑊
21	4, 12, 19, 20	fpwwe2 10638	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍𝑊(𝑊‘𝑍) ∧ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍) ↔ (𝑍 = 𝑍 ∧ (𝑊‘𝑍) = (𝑊‘𝑍))))
22	3, 21	mpbiri 258	. . . . . . . . 9 ⊢ (𝜑 → (𝑍𝑊(𝑊‘𝑍) ∧ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍))
23	22	simprd 497	. . . . . . . 8 ⊢ (𝜑 → (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍)
24	22	simpld 496	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍𝑊(𝑊‘𝑍))
25	4, 12	fpwwe2lem2 10627	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑍𝑊(𝑊‘𝑍) ↔ ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(^◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏))))
26	24, 25	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(^◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)))
27	26	simpld 496	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)))
28	27	simpld 496	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ 𝐴)
29	12, 28	ssexd 5325	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ V)
30		sseq1 4008	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑍 → (𝑎 ⊆ 𝐴 ↔ 𝑍 ⊆ 𝐴))
31		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑍 → 𝑎 = 𝑍)
32	31	sqxpeqd 5709	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑍 → (𝑎 × 𝑎) = (𝑍 × 𝑍))
33	32	sseq2d 4015	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑍 → ((𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ↔ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)))
34		weeq2 5666	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑍 → ((𝑊‘𝑍) We 𝑎 ↔ (𝑊‘𝑍) We 𝑍))
35	30, 33, 34	3anbi123d 1437	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑍 → ((𝑎 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ∧ (𝑊‘𝑍) We 𝑎) ↔ (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍)))
36	35	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑍 → ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ∧ (𝑊‘𝑍) We 𝑎)) ↔ (𝜑 ∧ (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))))
37		id 22	. . . . . . . . . . . . . . . 16 ⊢ ((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))
38	37	3expa 1119	. . . . . . . . . . . . . . 15 ⊢ (((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ (𝑊‘𝑍) We 𝑍) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))
39	38	adantrr 716	. . . . . . . . . . . . . 14 ⊢ (((𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍)) ∧ ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(^◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏)) → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))
40	26, 39	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍))
41	40	pm4.71i 561	. . . . . . . . . . . 12 ⊢ (𝜑 ↔ (𝜑 ∧ (𝑍 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑍 × 𝑍) ∧ (𝑊‘𝑍) We 𝑍)))
42	36, 41	bitr4di 289	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑍 → ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ∧ (𝑊‘𝑍) We 𝑎)) ↔ 𝜑))
43		oveq1 7416	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑍 → (𝑎𝐹(𝑊‘𝑍)) = (𝑍𝐹(𝑊‘𝑍)))
44	43, 31	eleq12d 2828	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑍 → ((𝑎𝐹(𝑊‘𝑍)) ∈ 𝑎 ↔ (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍))
45		breq1 5152	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑍 → (𝑎 ≺ ω ↔ 𝑍 ≺ ω))
46	44, 45	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑍 → (((𝑎𝐹(𝑊‘𝑍)) ∈ 𝑎 → 𝑎 ≺ ω) ↔ ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω)))
47	42, 46	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑎 = 𝑍 → (((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ∧ (𝑊‘𝑍) We 𝑎)) → ((𝑎𝐹(𝑊‘𝑍)) ∈ 𝑎 → 𝑎 ≺ ω)) ↔ (𝜑 → ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω))))
48		fvex 6905	. . . . . . . . . . 11 ⊢ (𝑊‘𝑍) ∈ V
49		sseq1 4008	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑊‘𝑍) → (𝑠 ⊆ (𝑎 × 𝑎) ↔ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎)))
50		weeq1 5665	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑊‘𝑍) → (𝑠 We 𝑎 ↔ (𝑊‘𝑍) We 𝑎))
51	49, 50	3anbi23d 1440	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑊‘𝑍) → ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ↔ (𝑎 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ∧ (𝑊‘𝑍) We 𝑎)))
52	51	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑊‘𝑍) → ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) ↔ (𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ∧ (𝑊‘𝑍) We 𝑎))))
53		oveq2 7417	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑊‘𝑍) → (𝑎𝐹𝑠) = (𝑎𝐹(𝑊‘𝑍)))
54	53	eleq1d 2819	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑊‘𝑍) → ((𝑎𝐹𝑠) ∈ 𝑎 ↔ (𝑎𝐹(𝑊‘𝑍)) ∈ 𝑎))
55	54	imbi1d 342	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑊‘𝑍) → (((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω) ↔ ((𝑎𝐹(𝑊‘𝑍)) ∈ 𝑎 → 𝑎 ≺ ω)))
56	52, 55	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑊‘𝑍) → (((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω)) ↔ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ∧ (𝑊‘𝑍) We 𝑎)) → ((𝑎𝐹(𝑊‘𝑍)) ∈ 𝑎 → 𝑎 ≺ ω))))
57		omelon 9641	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
58		onenon 9944	. . . . . . . . . . . . . . 15 ⊢ (ω ∈ On → ω ∈ dom card)
59	57, 58	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ω ∈ dom card
60		simpr3 1197	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑠 We 𝑎)
61	60	19.8ad 2176	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ∃𝑠 𝑠 We 𝑎)
62		ween 10030	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ dom card ↔ ∃𝑠 𝑠 We 𝑎)
63	61, 62	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → 𝑎 ∈ dom card)
64		domtri2 9984	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ dom card ∧ 𝑎 ∈ dom card) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω))
65	59, 63, 64	sylancr 588	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 ↔ ¬ 𝑎 ≺ ω))
66		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))
67		nfcv 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟𝑎
68		nfmpo2 7490	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑟(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))
69	18, 68	nfcxfr 2902	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟𝐹
70		nfcv 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑟𝑠
71	67, 69, 70	nfov 7439	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑟(𝑎𝐹𝑠)
72	71	nfel1 2920	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑟(𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)
73	66, 72	nfim 1900	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑟((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))
74		sseq1 4008	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑠 → (𝑟 ⊆ (𝑎 × 𝑎) ↔ 𝑠 ⊆ (𝑎 × 𝑎)))
75		weeq1 5665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑠 → (𝑟 We 𝑎 ↔ 𝑠 We 𝑎))
76	74, 75	3anbi23d 1440	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑠 → ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)))
77	76	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑠 → (((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)))
78	77	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑠 → ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎))))
79		oveq2 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑠 → (𝑎𝐹𝑟) = (𝑎𝐹𝑠))
80	79	eleq1d 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑠 → ((𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎) ↔ (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎)))
81	78, 80	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑠 → (((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))))
82		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))
83		nfcv 2904	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝑎
84		nfmpo1 7489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))
85	18, 84	nfcxfr 2902	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐹
86		nfcv 2904	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝑟
87	83, 85, 86	nfov 7439	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝑎𝐹𝑟)
88	87	nfel1 2920	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)
89	82, 88	nfim 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))
90		sseq1 4008	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 → (𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴))
91		xpeq12 5702	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 = 𝑎 ∧ 𝑥 = 𝑎) → (𝑥 × 𝑥) = (𝑎 × 𝑎))
92	91	anidms 568	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑎 → (𝑥 × 𝑥) = (𝑎 × 𝑎))
93	92	sseq2d 4015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑟 ⊆ (𝑎 × 𝑎)))
94		weeq2 5666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑎 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑎))
95	90, 93, 94	3anbi123d 1437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎)))
96		breq2 5153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → (ω ≼ 𝑥 ↔ ω ≼ 𝑎))
97	95, 96	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑎 → (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥) ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))
98	15, 97	bitrid 283	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑎 → (𝜓 ↔ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)))
99	98	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑎 → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎))))
100		oveq1 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑎 → (𝑥𝐹𝑟) = (𝑎𝐹𝑟))
101		difeq2 4117	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑎 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑎))
102	100, 101	eleq12d 2828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑎 → ((𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥) ↔ (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎)))
103	99, 102	imbi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑎 → (((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) ↔ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))))
104	5, 13, 14, 15, 16, 17, 18	pwfseqlem3 10655	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥))
105	89, 103, 104	chvarfv 2234	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑎 × 𝑎) ∧ 𝑟 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑟) ∈ (𝐴 ∖ 𝑎))
106	73, 81, 105	chvarfv 2234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → (𝑎𝐹𝑠) ∈ (𝐴 ∖ 𝑎))
107	106	eldifbd 3962	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎) ∧ ω ≼ 𝑎)) → ¬ (𝑎𝐹𝑠) ∈ 𝑎)
108	107	expr 458	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (ω ≼ 𝑎 → ¬ (𝑎𝐹𝑠) ∈ 𝑎))
109	65, 108	sylbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (¬ 𝑎 ≺ ω → ¬ (𝑎𝐹𝑠) ∈ 𝑎))
110	109	con4d 115	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → ((𝑎𝐹𝑠) ∈ 𝑎 → 𝑎 ≺ ω))
111	48, 56, 110	vtocl 3550	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ (𝑊‘𝑍) ⊆ (𝑎 × 𝑎) ∧ (𝑊‘𝑍) We 𝑎)) → ((𝑎𝐹(𝑊‘𝑍)) ∈ 𝑎 → 𝑎 ≺ ω))
112	47, 111	vtoclg 3557	. . . . . . . . 9 ⊢ (𝑍 ∈ V → (𝜑 → ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω)))
113	29, 112	mpcom 38	. . . . . . . 8 ⊢ (𝜑 → ((𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 → 𝑍 ≺ ω))
114	23, 113	mpd 15	. . . . . . 7 ⊢ (𝜑 → 𝑍 ≺ ω)
115		isfinite 9647	. . . . . . 7 ⊢ (𝑍 ∈ Fin ↔ 𝑍 ≺ ω)
116	114, 115	sylibr 233	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ Fin)
117	5, 13, 14, 15, 16, 17, 18	pwfseqlem2 10654	. . . . . 6 ⊢ ((𝑍 ∈ Fin ∧ (𝑊‘𝑍) ∈ V) → (𝑍𝐹(𝑊‘𝑍)) = (𝐻‘(card‘𝑍)))
118	116, 48, 117	sylancl 587	. . . . 5 ⊢ (𝜑 → (𝑍𝐹(𝑊‘𝑍)) = (𝐻‘(card‘𝑍)))
119	118, 23	eqeltrrd 2835	. . . 4 ⊢ (𝜑 → (𝐻‘(card‘𝑍)) ∈ 𝑍)
120	4, 12, 24	fpwwe2lem3 10628	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐻‘(card‘𝑍)) ∈ 𝑍) → ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘𝑍)))
121	119, 120	mpdan 686	. . . . . . . . 9 ⊢ (𝜑 → ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘𝑍)))
122		cnvimass 6081	. . . . . . . . . . . 12 ⊢ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ dom (𝑊‘𝑍)
123	27	simprd 497	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊‘𝑍) ⊆ (𝑍 × 𝑍))
124		dmss 5903	. . . . . . . . . . . . . 14 ⊢ ((𝑊‘𝑍) ⊆ (𝑍 × 𝑍) → dom (𝑊‘𝑍) ⊆ dom (𝑍 × 𝑍))
125	123, 124	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑊‘𝑍) ⊆ dom (𝑍 × 𝑍))
126		dmxpss 6171	. . . . . . . . . . . . 13 ⊢ dom (𝑍 × 𝑍) ⊆ 𝑍
127	125, 126	sstrdi 3995	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (𝑊‘𝑍) ⊆ 𝑍)
128	122, 127	sstrid 3994	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍)
129	116, 128	ssfid 9267	. . . . . . . . . 10 ⊢ (𝜑 → (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin)
130	48	inex1 5318	. . . . . . . . . 10 ⊢ ((𝑊‘𝑍) ∩ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ∈ V
131	5, 13, 14, 15, 16, 17, 18	pwfseqlem2 10654	. . . . . . . . . 10 ⊢ (((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin ∧ ((𝑊‘𝑍) ∩ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ∈ V) → ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
132	129, 130, 131	sylancl 587	. . . . . . . . 9 ⊢ (𝜑 → ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})𝐹((𝑊‘𝑍) ∩ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) × (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))) = (𝐻‘(card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
133	121, 132	eqtr3d 2775	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘(card‘𝑍)) = (𝐻‘(card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
134		f1of1 6833	. . . . . . . . . 10 ⊢ (𝐻:ω–1-1-onto→𝑋 → 𝐻:ω–1-1→𝑋)
135	14, 134	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:ω–1-1→𝑋)
136		ficardom 9956	. . . . . . . . . 10 ⊢ (𝑍 ∈ Fin → (card‘𝑍) ∈ ω)
137	116, 136	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (card‘𝑍) ∈ ω)
138		ficardom 9956	. . . . . . . . . 10 ⊢ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin → (card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)
139	129, 138	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)
140		f1fveq 7261	. . . . . . . . 9 ⊢ ((𝐻:ω–1-1→𝑋 ∧ ((card‘𝑍) ∈ ω ∧ (card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) ∈ ω)) → ((𝐻‘(card‘𝑍)) = (𝐻‘(card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ↔ (card‘𝑍) = (card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
141	135, 137, 139, 140	syl12anc 836	. . . . . . . 8 ⊢ (𝜑 → ((𝐻‘(card‘𝑍)) = (𝐻‘(card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))) ↔ (card‘𝑍) = (card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))))
142	133, 141	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (card‘𝑍) = (card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})))
143	142	eqcomd 2739	. . . . . 6 ⊢ (𝜑 → (card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍))
144		finnum 9943	. . . . . . . 8 ⊢ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ Fin → (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card)
145	129, 144	syl 17	. . . . . . 7 ⊢ (𝜑 → (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card)
146		finnum 9943	. . . . . . . 8 ⊢ (𝑍 ∈ Fin → 𝑍 ∈ dom card)
147	116, 146	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ dom card)
148		carden2 9982	. . . . . . 7 ⊢ (((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ∈ dom card ∧ 𝑍 ∈ dom card) → ((card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍) ↔ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
149	145, 147, 148	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ((card‘(^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))})) = (card‘𝑍) ↔ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
150	143, 149	mpbid 231	. . . . 5 ⊢ (𝜑 → (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
151		dfpss2 4086	. . . . . . . 8 ⊢ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍 ∧ ¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
152	151	baib 537	. . . . . . 7 ⊢ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊆ 𝑍 → ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
153	128, 152	syl 17	. . . . . 6 ⊢ (𝜑 → ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 ↔ ¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍))
154		php3 9212	. . . . . . . . 9 ⊢ ((𝑍 ∈ Fin ∧ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍) → (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≺ 𝑍)
155		sdomnen 8977	. . . . . . . . 9 ⊢ ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≺ 𝑍 → ¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
156	154, 155	syl 17	. . . . . . . 8 ⊢ ((𝑍 ∈ Fin ∧ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍) → ¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍)
157	156	ex 414	. . . . . . 7 ⊢ (𝑍 ∈ Fin → ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 → ¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
158	116, 157	syl 17	. . . . . 6 ⊢ (𝜑 → ((^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ⊊ 𝑍 → ¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
159	153, 158	sylbird 260	. . . . 5 ⊢ (𝜑 → (¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍 → ¬ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ≈ 𝑍))
160	150, 159	mt4d 117	. . . 4 ⊢ (𝜑 → (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) = 𝑍)
161	119, 160	eleqtrrd 2837	. . 3 ⊢ (𝜑 → (𝐻‘(card‘𝑍)) ∈ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}))
162		fvex 6905	. . . 4 ⊢ (𝐻‘(card‘𝑍)) ∈ V
163	162	eliniseg 6094	. . . 4 ⊢ ((𝐻‘(card‘𝑍)) ∈ V → ((𝐻‘(card‘𝑍)) ∈ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ↔ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍))))
164	162, 163	ax-mp 5	. . 3 ⊢ ((𝐻‘(card‘𝑍)) ∈ (^◡(𝑊‘𝑍) “ {(𝐻‘(card‘𝑍))}) ↔ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))
165	161, 164	sylib 217	. 2 ⊢ (𝜑 → (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))
166	26	simprd 497	. . . . 5 ⊢ (𝜑 → ((𝑊‘𝑍) We 𝑍 ∧ ∀𝑏 ∈ 𝑍 [(^◡(𝑊‘𝑍) “ {𝑏}) / 𝑣](𝑣𝐹((𝑊‘𝑍) ∩ (𝑣 × 𝑣))) = 𝑏))
167	166	simpld 496	. . . 4 ⊢ (𝜑 → (𝑊‘𝑍) We 𝑍)
168		weso 5668	. . . 4 ⊢ ((𝑊‘𝑍) We 𝑍 → (𝑊‘𝑍) Or 𝑍)
169	167, 168	syl 17	. . 3 ⊢ (𝜑 → (𝑊‘𝑍) Or 𝑍)
170		sonr 5612	. . 3 ⊢ (((𝑊‘𝑍) Or 𝑍 ∧ (𝐻‘(card‘𝑍)) ∈ 𝑍) → ¬ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))
171	169, 119, 170	syl2anc 585	. 2 ⊢ (𝜑 → ¬ (𝐻‘(card‘𝑍))(𝑊‘𝑍)(𝐻‘(card‘𝑍)))
172	165, 171	pm2.65i 193	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∀wral 3062 {crab 3433 Vcvv 3475 [wsbc 3778 ∖ cdif 3946 ∩ cin 3948 ⊆ wss 3949 ⊊ wpss 3950 ifcif 4529 𝒫 cpw 4603 {csn 4629 ∪ cuni 4909 ∩ cint 4951 ∪ ciun 4998 class class class wbr 5149 {copab 5211 Or wor 5588 We wwe 5631 × cxp 5675 ^◡ccnv 5676 dom cdm 5677 ran crn 5678 “ cima 5680 Oncon0 6365 –1-1→wf1 6541 –1-1-onto→wf1o 6543 ‘cfv 6544 (class class class)co 7409 ∈ cmpo 7411 ωcom 7855 ↑_m cmap 8820 ≈ cen 8936 ≼ cdom 8937 ≺ csdm 8938 Fincfn 8939 cardccrd 9930

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-inf2 9636

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-oi 9505 df-card 9934

This theorem is referenced by: pwfseqlem5 10658

W3C validator