iunfictbso - Metamath Proof Explorer

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

Theorem iunfictbso 10038

Description: Countability of a countable union of finite sets with a strict (not globally well) order fulfilling the choice role. (Contributed by Stefan O'Rear, 16-Nov-2014.)

**Assertion**
Ref	Expression
iunfictbso	⊢ ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω)

Proof of Theorem iunfictbso Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		omex 9566	. . . . 5 ⊢ ω ∈ V
2	1	0dom 9049	. . . 4 ⊢ ∅ ≼ ω
3		breq1 5103	. . . 4 ⊢ (∪ 𝐴 = ∅ → (∪ 𝐴 ≼ ω ↔ ∅ ≼ ω))
4	2, 3	mpbiri 258	. . 3 ⊢ (∪ 𝐴 = ∅ → ∪ 𝐴 ≼ ω)
5	4	a1d 25	. 2 ⊢ (∪ 𝐴 = ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
6		n0 4307	. . 3 ⊢ (∪ 𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ ∪ 𝐴)
7		ne0i 4295	. . . . . . . . . 10 ⊢ (𝑎 ∈ ∪ 𝐴 → ∪ 𝐴 ≠ ∅)
8		unieq 4876	. . . . . . . . . . . 12 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
9		uni0 4893	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
10	8, 9	eqtrdi 2788	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
11	10	necon3i 2965	. . . . . . . . . 10 ⊢ (∪ 𝐴 ≠ ∅ → 𝐴 ≠ ∅)
12	7, 11	syl 17	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ 𝐴 → 𝐴 ≠ ∅)
13	12	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≠ ∅)
14		simpl1 1193	. . . . . . . . 9 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≼ ω)
15		ctex 8914	. . . . . . . . 9 ⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
16		0sdomg 9048	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
17	14, 15, 16	3syl 18	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
18	13, 17	mpbird 257	. . . . . . 7 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∅ ≺ 𝐴)
19		fodomr 9070	. . . . . . 7 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ω) → ∃𝑏 𝑏:ω–onto→𝐴)
20	18, 14, 19	syl2anc 585	. . . . . 6 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∃𝑏 𝑏:ω–onto→𝐴)
21		omelon 9569	. . . . . . . . . . . 12 ⊢ ω ∈ On
22		onenon 9875	. . . . . . . . . . . 12 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . 11 ⊢ ω ∈ dom card
24		xpnum 9877	. . . . . . . . . . 11 ⊢ ((ω ∈ dom card ∧ ω ∈ dom card) → (ω × ω) ∈ dom card)
25	23, 23, 24	mp2an 693	. . . . . . . . . 10 ⊢ (ω × ω) ∈ dom card
26		simplrr 778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω–onto→𝐴)
27		fof 6756	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏:ω–onto→𝐴 → 𝑏:ω⟶𝐴)
28	26, 27	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω⟶𝐴)
29		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑓 ∈ ω)
30	28, 29	ffvelcdmd 7041	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ 𝐴)
31	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ∈ 𝐴)
32		elssuni 4896	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏‘𝑓) ∈ 𝐴 → (𝑏‘𝑓) ⊆ ∪ 𝐴)
33	31, 32	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ⊆ ∪ 𝐴)
34	30, 32	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ⊆ ∪ 𝐴)
35		simpll3 1216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or ∪ 𝐴)
36		soss 5562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏‘𝑓) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑓)))
37	34, 35, 36	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or (𝑏‘𝑓))
38		simpll2 1215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐴 ⊆ Fin)
39	38, 30	sseldd 3936	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ Fin)
40		finnisoeu 10037	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 Or (𝑏‘𝑓) ∧ (𝑏‘𝑓) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
41	37, 39, 40	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
42		iotacl 6488	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))})
43	41, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))})
44		iotaex 6478	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ V
45		isoeq1 7275	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))))
46		isoeq1 7275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))))
47	46	cbvabv 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))}
48	44, 45, 47	elab2 3639	. . . . . . . . . . . . . . . . . 18 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
49	43, 48	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
50		isof1o 7281	. . . . . . . . . . . . . . . . 17 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓))
51		f1of 6784	. . . . . . . . . . . . . . . . 17 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))⟶(𝑏‘𝑓))
52	49, 50, 51	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))⟶(𝑏‘𝑓))
53	52	ffvelcdmda 7040	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ (𝑏‘𝑓))
54	33, 53	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ ∪ 𝐴)
55		simprl 771	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → 𝑎 ∈ ∪ 𝐴)
56	55	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ ¬ 𝑔 ∈ (card‘(𝑏‘𝑓))) → 𝑎 ∈ ∪ 𝐴)
57	54, 56	ifclda 4517	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴)
58	57	ralrimivva 3181	. . . . . . . . . . . 12 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴)
59		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)) = (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))
60	59	fmpo 8024	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴 ↔ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴)
61	58, 60	sylib 218	. . . . . . . . . . 11 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴)
62		eluni 4868	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ ∪ 𝐴 ↔ ∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴))
63		simplrr 778	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑏:ω–onto→𝐴)
64		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑖 ∈ 𝐴)
65		foelrn 7063	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏:ω–onto→𝐴 ∧ 𝑖 ∈ 𝐴) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗))
66	63, 64, 65	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗))
67		simprrl 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑗 ∈ ω)
68		ordom 7830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ord ω
69		simpll2 1215	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐴 ⊆ Fin)
70		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω–onto→𝐴)
71	70, 27	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω⟶𝐴)
72	71, 67	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ 𝐴)
73	69, 72	sseldd 3936	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ Fin)
74		ficardom 9887	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑗) ∈ Fin → (card‘(𝑏‘𝑗)) ∈ ω)
75	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ∈ ω)
76		ordelss 6343	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord ω ∧ (card‘(𝑏‘𝑗)) ∈ ω) → (card‘(𝑏‘𝑗)) ⊆ ω)
77	68, 75, 76	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ⊆ ω)
78		elssuni 4896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏‘𝑗) ∈ 𝐴 → (𝑏‘𝑗) ⊆ ∪ 𝐴)
79	72, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ⊆ ∪ 𝐴)
80		simpll3 1216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or ∪ 𝐴)
81		soss 5562	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏‘𝑗) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑗)))
82	79, 80, 81	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or (𝑏‘𝑗))
83		finnisoeu 10037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 Or (𝑏‘𝑗) ∧ (𝑏‘𝑗) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
84	82, 73, 83	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
85		iotacl 6488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))})
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))})
87		iotaex 6478	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ V
88		isoeq1 7275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
89		isoeq1 7275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
90	89	cbvabv 2807	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))}
91	87, 88, 90	elab2 3639	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
92	86, 91	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
93		isof1o 7281	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗))
95		f1ocnv 6796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) → ^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗)))
96		f1of 6784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗)) → ^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)⟶(card‘(𝑏‘𝑗)))
97	94, 95, 96	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)⟶(card‘(𝑏‘𝑗)))
98		simprll 779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ 𝑖)
99		simprrr 782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑖 = (𝑏‘𝑗))
100	98, 99	eleqtrd 2839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ (𝑏‘𝑗))
101	97, 100	ffvelcdmd 7041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)))
102	77, 101	sseldd 3936	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω)
103		2fveq3 6849	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑗 → (card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)))
104	103	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑗 → (𝑔 ∈ (card‘(𝑏‘𝑓)) ↔ 𝑔 ∈ (card‘(𝑏‘𝑗))))
105		isoeq4 7278	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓))))
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓))))
107		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = 𝑗 → (𝑏‘𝑓) = (𝑏‘𝑗))
108		isoeq5 7279	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏‘𝑓) = (𝑏‘𝑗) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
110	106, 109	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
111	110	iotabidv 6486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑗 → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
112	111	fveq1d 6846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑗 → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔))
113	104, 112	ifbieq1d 4506	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑗 → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) = if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎))
114		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → (𝑔 ∈ (card‘(𝑏‘𝑗)) ↔ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗))))
115		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
116	114, 115	ifbieq1d 4506	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎) = if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎))
117		fvex 6857	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) ∈ V
118		vex 3446	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑎 ∈ V
119	117, 118	ifex 4532	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) ∈ V
120	113, 116, 59, 119	ovmpo 7530	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ ω ∧ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎))
121	67, 102, 120	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎))
122	101	iftrued 4489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
123		f1ocnvfv2 7235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) ∧ 𝑐 ∈ (𝑏‘𝑗)) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐)
124	94, 100, 123	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐)
125	121, 122, 124	3eqtrrd 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
126		rspceov 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ ω ∧ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω ∧ 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
127	67, 102, 125, 126	syl3anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
128	127	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ((𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
129	128	expd 415	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (𝑗 ∈ ω → (𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))))
130	129	rexlimdv 3137	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
131	66, 130	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
132	131	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
133	132	exlimdv 1935	. . . . . . . . . . . . 13 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
134	62, 133	biimtrid 242	. . . . . . . . . . . 12 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑐 ∈ ∪ 𝐴 → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
135	134	ralrimiv 3129	. . . . . . . . . . 11 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
136		foov 7544	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 ↔ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴 ∧ ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))
137	61, 135, 136	sylanbrc 584	. . . . . . . . . 10 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴)
138		fodomnum 9981	. . . . . . . . . 10 ⊢ ((ω × ω) ∈ dom card → ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 → ∪ 𝐴 ≼ (ω × ω)))
139	25, 137, 138	mpsyl 68	. . . . . . . . 9 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ (ω × ω))
140		xpomen 9939	. . . . . . . . 9 ⊢ (ω × ω) ≈ ω
141		domentr 8964	. . . . . . . . 9 ⊢ ((∪ 𝐴 ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → ∪ 𝐴 ≼ ω)
142	139, 140, 141	sylancl 587	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ ω)
143	142	expr 456	. . . . . . 7 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼ ω))
144	143	exlimdv 1935	. . . . . 6 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∃𝑏 𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼ ω))
145	20, 144	mpd 15	. . . . 5 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∪ 𝐴 ≼ ω)
146	145	expcom 413	. . . 4 ⊢ (𝑎 ∈ ∪ 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
147	146	exlimiv 1932	. . 3 ⊢ (∃𝑎 𝑎 ∈ ∪ 𝐴 → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
148	6, 147	sylbi 217	. 2 ⊢ (∪ 𝐴 ≠ ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
149	5, 148	pm2.61ine 3016	1 ⊢ ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∃!weu 2569 {cab 2715 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ⊆ wss 3903 ∅c0 4287 ifcif 4481 ∪ cuni 4865 class class class wbr 5100 E cep 5533 Or wor 5541 × cxp 5632 ^◡ccnv 5633 dom cdm 5634 Ord word 6326 Oncon0 6327 ℩cio 6456 ⟶wf 6498 –onto→wfo 6500 –1-1-onto→wf1o 6501 ‘cfv 6502 Isom wiso 6503 (class class class)co 7370 ∈ cmpo 7372 ωcom 7820 ≈ cen 8894 ≼ cdom 8895 ≺ csdm 8896 Fincfn 8897 cardccrd 9861

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-inf2 9564

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-se 5588 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-isom 6511 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7821 df-1st 7945 df-2nd 7946 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-oadd 8413 df-omul 8414 df-er 8647 df-map 8779 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-oi 9429 df-card 9865 df-acn 9868

This theorem is referenced by: aannenlem3 26311

W3C validator