Theorem fin23lem27 10241

Description: The mapping constructed in fin23lem22 10240 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014.)

Hypothesis

Ref	Expression
fin23lem22.b	⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))

Assertion

Ref	Expression
fin23lem27	⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))

Distinct variable group:   𝑖,𝑗,𝑆

Allowed substitution hints:   𝐶(𝑖,𝑗)

Proof of Theorem fin23lem27

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordom 7816	. . . 4 ⊢ Ord ω
2		ordwe 6323	. . . 4 ⊢ (Ord ω → E We ω)
3		weso 5609	. . . 4 ⊢ ( E We ω → E Or ω)
4	1, 2, 3	mp2b 10	. . 3 ⊢ E Or ω
5	4	a1i 11	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6		sopo 5545	. . . . 5 ⊢ ( E Or ω → E Po ω)
7	4, 6	ax-mp 5	. . . 4 ⊢ E Po ω
8		poss 5528	. . . 4 ⊢ (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
9	7, 8	mpi 20	. . 3 ⊢ (𝑆 ⊆ ω → E Po 𝑆)
10	9	adantr 481	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11		fin23lem22.b	. . . 4 ⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
12	11	fin23lem22 10240	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto→𝑆)
13		f1ofo 6774	. . 3 ⊢ (𝐶:ω–1-1-onto→𝑆 → 𝐶:ω–onto→𝑆)
14	12, 13	syl 17	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto→𝑆)
15		nnsdomel 9905	. . . . . . . 8 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏))
16	15	adantl 482	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏))
17	16	biimpd 230	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → 𝑎 ≺ 𝑏))
18		fin23lem23 10239	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)
19	18	adantrr 723	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)
20		ineq1 4142	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (𝑗 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	breq1d 5082	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑎 ↔ (𝑖 ∩ 𝑆) ≈ 𝑎))
22	21	cbvreuvw 3366	. . . . . . . . . . . 12 ⊢ (∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
23	19, 22	sylib 219	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
24		nfv 1921	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
25	21	cbvriotavw 7323	. . . . . . . . . . . 12 ⊢ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
26		ineq1 4142	. . . . . . . . . . . . 13 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆))
27	26	breq1d 5082	. . . . . . . . . . . 12 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → ((𝑖 ∩ 𝑆) ≈ 𝑎 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
28	24, 25, 27	riotaprop 7340	. . . . . . . . . . 11 ⊢ (∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
29	23, 28	syl 17	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
30	29	simprd 496	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
31	30	adantrr 723	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32		simprr 778	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ 𝑏)
33		fin23lem23 10239	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)
34	33	adantrl 722	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)
35	20	breq1d 5082	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑏 ↔ (𝑖 ∩ 𝑆) ≈ 𝑏))
36	35	cbvreuvw 3366	. . . . . . . . . . . . . 14 ⊢ (∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
37	34, 36	sylib 219	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
38		nfv 1921	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
39	35	cbvriotavw 7323	. . . . . . . . . . . . . 14 ⊢ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
40		ineq1 4142	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
41	40	breq1d 5082	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → ((𝑖 ∩ 𝑆) ≈ 𝑏 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
42	38, 39, 41	riotaprop 7340	. . . . . . . . . . . . 13 ⊢ (∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
44	43	simprd 496	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
45	44	ensymd 8942	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
46	45	adantrr 723	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
47		sdomentr 9039	. . . . . . . . 9 ⊢ ((𝑎 ≺ 𝑏 ∧ 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
48	32, 46, 47	syl2anc 590	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
49		ensdomtr 9041	. . . . . . . 8 ⊢ ((((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎 ∧ 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
50	31, 48, 49	syl2anc 590	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
51	50	expr 457	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ≺ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)))
52		simpll 772	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53		omsson 7810	. . . . . . . . 9 ⊢ ω ⊆ On
54	52, 53	sstrdi 3927	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
55	29	simpld 495	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆)
56	54, 55	sseldd 3916	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On)
57	43	simpld 495	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆)
58	54, 57	sseldd 3916	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On)
59		onsdominel 9054	. . . . . . . 8 ⊢ (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
60	59	3expia 1127	. . . . . . 7 ⊢ (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
61	56, 58, 60	syl2anc 590	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
62	17, 51, 61	3syld 60	. . . . 5 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
63		breq2 5076	. . . . . . . 8 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
64	63	riotabidv 7315	. . . . . . 7 ⊢ (𝑖 = 𝑎 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
65		simprl 776	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
66	11, 64, 65, 55	fvmptd3 6959	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑎) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
67		breq2 5076	. . . . . . . 8 ⊢ (𝑖 = 𝑏 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑏))
68	67	riotabidv 7315	. . . . . . 7 ⊢ (𝑖 = 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
69		simprr 778	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
70	11, 68, 69, 57	fvmptd3 6959	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑏) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
71	66, 70	eleq12d 2833	. . . . 5 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶‘𝑎) ∈ (𝐶‘𝑏) ↔ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
72	62, 71	sylibrd 260	. . . 4 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (𝐶‘𝑎) ∈ (𝐶‘𝑏)))
73		epel 5521	. . . 4 ⊢ (𝑎 E 𝑏 ↔ 𝑎 ∈ 𝑏)
74		fvex 6840	. . . . 5 ⊢ (𝐶‘𝑏) ∈ V
75	74	epeli 5520	. . . 4 ⊢ ((𝐶‘𝑎) E (𝐶‘𝑏) ↔ (𝐶‘𝑎) ∈ (𝐶‘𝑏))
76	72, 73, 75	3imtr4g 297	. . 3 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))
77	76	ralrimivva 3182	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))
78		soisoi 7272	. 2 ⊢ ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto→𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
79	5, 10, 14, 77, 78	syl22anc 844	1 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∃!wreu 3342   ∩ cin 3882   ⊆ wss 3883   class class class wbr 5072   ↦ cmpt 5153   E cep 5517   Po wpo 5524   Or wor 5525   We wwe 5570  Ord word 6309  Oncon0 6310  –onto→wfo 6483  –1-1-onto→wf1o 6484  ‘cfv 6485   Isom wiso 6486  ℩crio 7312  ωcom 7806   ≈ cen 8880   ≺ csdm 8882  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-1o 8395  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9854

This theorem is referenced by: (None)