Theorem fin23lem27 10238

Description: The mapping constructed in fin23lem22 10237 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 7818	. . . 4 ⊢ Ord ω
2		ordwe 6330	. . . 4 ⊢ (Ord ω → E We ω)
3		weso 5615	. . . 4 ⊢ ( E We ω → E Or ω)
4	1, 2, 3	mp2b 10	. . 3 ⊢ E Or ω
5	4	a1i 11	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Or ω)
6		sopo 5551	. . . . 5 ⊢ ( E Or ω → E Po ω)
7	4, 6	ax-mp 5	. . . 4 ⊢ E Po ω
8		poss 5534	. . . 4 ⊢ (𝑆 ⊆ ω → ( E Po ω → E Po 𝑆))
9	7, 8	mpi 20	. . 3 ⊢ (𝑆 ⊆ ω → E Po 𝑆)
10	9	adantr 480	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → E Po 𝑆)
11		fin23lem22.b	. . . 4 ⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))
12	11	fin23lem22 10237	. . 3 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto→𝑆)
13		f1ofo 6781	. . 3 ⊢ (𝐶:ω–1-1-onto→𝑆 → 𝐶:ω–onto→𝑆)
14	12, 13	syl 17	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–onto→𝑆)
15		nnsdomel 9902	. . . . . . . 8 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏))
16	15	adantl 481	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏))
17	16	biimpd 229	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → 𝑎 ≺ 𝑏))
18		fin23lem23 10236	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)
19	18	adantrr 717	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)
20		ineq1 4165	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (𝑗 ∩ 𝑆) = (𝑖 ∩ 𝑆))
21	20	breq1d 5108	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑎 ↔ (𝑖 ∩ 𝑆) ≈ 𝑎))
22	21	cbvreuvw 3372	. . . . . . . . . . . 12 ⊢ (∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
23	19, 22	sylib 218	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
24		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎
25	21	cbvriotavw 7325	. . . . . . . . . . . 12 ⊢ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎)
26		ineq1 4165	. . . . . . . . . . . . 13 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆))
27	26	breq1d 5108	. . . . . . . . . . . 12 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → ((𝑖 ∩ 𝑆) ≈ 𝑎 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
28	24, 25, 27	riotaprop 7342	. . . . . . . . . . 11 ⊢ (∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
29	23, 28	syl 17	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎))
30	29	simprd 495	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
31	30	adantrr 717	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)
32		simprr 772	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ 𝑏)
33		fin23lem23 10236	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)
34	33	adantrl 716	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)
35	20	breq1d 5108	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑏 ↔ (𝑖 ∩ 𝑆) ≈ 𝑏))
36	35	cbvreuvw 3372	. . . . . . . . . . . . . 14 ⊢ (∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
37	34, 36	sylib 218	. . . . . . . . . . . . 13 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
38		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏
39	35	cbvriotavw 7325	. . . . . . . . . . . . . 14 ⊢ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏)
40		ineq1 4165	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
41	40	breq1d 5108	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → ((𝑖 ∩ 𝑆) ≈ 𝑏 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
42	38, 39, 41	riotaprop 7342	. . . . . . . . . . . . 13 ⊢ (∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏))
44	43	simprd 495	. . . . . . . . . . 11 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)
45	44	ensymd 8942	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
46	45	adantrr 717	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
47		sdomentr 9039	. . . . . . . . 9 ⊢ ((𝑎 ≺ 𝑏 ∧ 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
48	32, 46, 47	syl2anc 584	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
49		ensdomtr 9041	. . . . . . . 8 ⊢ ((((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎 ∧ 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
50	31, 48, 49	syl2anc 584	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))
51	50	expr 456	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ≺ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)))
52		simpll 766	. . . . . . . . 9 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ ω)
53		omsson 7812	. . . . . . . . 9 ⊢ ω ⊆ On
54	52, 53	sstrdi 3946	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On)
55	29	simpld 494	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆)
56	54, 55	sseldd 3934	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On)
57	43	simpld 494	. . . . . . . 8 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆)
58	54, 57	sseldd 3934	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On)
59		onsdominel 9054	. . . . . . . 8 ⊢ (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
60	59	3expia 1121	. . . . . . 7 ⊢ (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
61	56, 58, 60	syl2anc 584	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
62	17, 51, 61	3syld 60	. . . . 5 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
63		breq2 5102	. . . . . . . 8 ⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎))
64	63	riotabidv 7317	. . . . . . 7 ⊢ (𝑖 = 𝑎 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
65		simprl 770	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈ ω)
66	11, 64, 65, 55	fvmptd3 6964	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑎) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎))
67		breq2 5102	. . . . . . . 8 ⊢ (𝑖 = 𝑏 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑏))
68	67	riotabidv 7317	. . . . . . 7 ⊢ (𝑖 = 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
69		simprr 772	. . . . . . 7 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈ ω)
70	11, 68, 69, 57	fvmptd3 6964	. . . . . 6 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑏) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))
71	66, 70	eleq12d 2830	. . . . 5 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶‘𝑎) ∈ (𝐶‘𝑏) ↔ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)))
72	62, 71	sylibrd 259	. . . 4 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (𝐶‘𝑎) ∈ (𝐶‘𝑏)))
73		epel 5527	. . . 4 ⊢ (𝑎 E 𝑏 ↔ 𝑎 ∈ 𝑏)
74		fvex 6847	. . . . 5 ⊢ (𝐶‘𝑏) ∈ V
75	74	epeli 5526	. . . 4 ⊢ ((𝐶‘𝑎) E (𝐶‘𝑏) ↔ (𝐶‘𝑎) ∈ (𝐶‘𝑏))
76	72, 73, 75	3imtr4g 296	. . 3 ⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))
77	76	ralrimivva 3179	. 2 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))
78		soisoi 7274	. 2 ⊢ ((( E Or ω ∧ E Po 𝑆) ∧ (𝐶:ω–onto→𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))) → 𝐶 Isom E , E (ω, 𝑆))
79	5, 10, 14, 77, 78	syl22anc 838	1 ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∃!wreu 3348   ∩ cin 3900   ⊆ wss 3901   class class class wbr 5098   ↦ cmpt 5179   E cep 5523   Po wpo 5530   Or wor 5531   We wwe 5576  Ord word 6316  Oncon0 6317  –onto→wfo 6490  –1-1-onto→wf1o 6491  ‘cfv 6492   Isom wiso 6493  ℩crio 7314  ωcom 7808   ≈ 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-1o 8397  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9851

This theorem is referenced by: (None)