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 10026

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 9554	. . . . 5 ⊢ ω ∈ V
2	1	0dom 9037	. . . 4 ⊢ ∅ ≼ ω
3		breq1 5100	. . . 4 ⊢ (∪ 𝐴 = ∅ → (∪ 𝐴 ≼ ω ↔ ∅ ≼ ω))
4	2, 3	mpbiri 258	. . 3 ⊢ (∪ 𝐴 = ∅ → ∪ 𝐴 ≼ ω)
5	4	a1d 25	. 2 ⊢ (∪ 𝐴 = ∅ → ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω))
6		n0 4304	. . 3 ⊢ (∪ 𝐴 ≠ ∅ ↔ ∃𝑎 𝑎 ∈ ∪ 𝐴)
7		ne0i 4292	. . . . . . . . . 10 ⊢ (𝑎 ∈ ∪ 𝐴 → ∪ 𝐴 ≠ ∅)
8		unieq 4873	. . . . . . . . . . . 12 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅)
9		uni0 4890	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
10	8, 9	eqtrdi 2786	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∅)
11	10	necon3i 2963	. . . . . . . . . 10 ⊢ (∪ 𝐴 ≠ ∅ → 𝐴 ≠ ∅)
12	7, 11	syl 17	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ 𝐴 → 𝐴 ≠ ∅)
13	12	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≠ ∅)
14		simpl1 1193	. . . . . . . . 9 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≼ ω)
15		ctex 8902	. . . . . . . . 9 ⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
16		0sdomg 9036	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
17	14, 15, 16	3syl 18	. . . . . . . 8 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
18	13, 17	mpbird 257	. . . . . . 7 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∅ ≺ 𝐴)
19		fodomr 9058	. . . . . . 7 ⊢ ((∅ ≺ 𝐴 ∧ 𝐴 ≼ ω) → ∃𝑏 𝑏:ω–onto→𝐴)
20	18, 14, 19	syl2anc 585	. . . . . 6 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∃𝑏 𝑏:ω–onto→𝐴)
21		omelon 9557	. . . . . . . . . . . 12 ⊢ ω ∈ On
22		onenon 9863	. . . . . . . . . . . 12 ⊢ (ω ∈ On → ω ∈ dom card)
23	21, 22	ax-mp 5	. . . . . . . . . . 11 ⊢ ω ∈ dom card
24		xpnum 9865	. . . . . . . . . . 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 6745	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏:ω–onto→𝐴 → 𝑏:ω⟶𝐴)
28	26, 27	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω⟶𝐴)
29		simprl 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑓 ∈ ω)
30	28, 29	ffvelcdmd 7030	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ 𝐴)
31	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ∈ 𝐴)
32		elssuni 4893	. . . . . . . . . . . . . . . 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 5551	. . . . . . . . . . . . . . . . . . . . 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 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ Fin)
40		finnisoeu 10025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 Or (𝑏‘𝑓) ∧ (𝑏‘𝑓) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
41	37, 39, 40	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))
42		iotacl 6477	. . . . . . . . . . . . . . . . . . 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 6467	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ V
45		isoeq1 7263	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))))
46		isoeq1 7263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))))
47	46	cbvabv 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))}
48	44, 45, 47	elab2 3636	. . . . . . . . . . . . . . . . . 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 7269	. . . . . . . . . . . . . . . . 17 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓))
51		f1of 6773	. . . . . . . . . . . . . . . . 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 7029	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ (𝑏‘𝑓))
54	33, 53	sseldd 3933	. . . . . . . . . . . . . 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 4514	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴)
58	57	ralrimivva 3178	. . . . . . . . . . . 12 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴)
59		eqid 2735	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)) = (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))
60	59	fmpo 8012	. . . . . . . . . . . 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 4865	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ ∪ 𝐴 ↔ ∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴))
63		simplrr 778	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑏:ω–onto→𝐴)
64		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑖 ∈ 𝐴)
65		foelrn 7052	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏:ω–onto→𝐴 ∧ 𝑖 ∈ 𝐴) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗))
66	63, 64, 65	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗))
67		simprrl 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑗 ∈ ω)
68		ordom 7818	. . . . . . . . . . . . . . . . . . . . . 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 7030	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ 𝐴)
73	69, 72	sseldd 3933	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ Fin)
74		ficardom 9875	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑗) ∈ Fin → (card‘(𝑏‘𝑗)) ∈ ω)
75	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ∈ ω)
76		ordelss 6332	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord ω ∧ (card‘(𝑏‘𝑗)) ∈ ω) → (card‘(𝑏‘𝑗)) ⊆ ω)
77	68, 75, 76	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ⊆ ω)
78		elssuni 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏‘𝑗) ∈ 𝐴 → (𝑏‘𝑗) ⊆ ∪ 𝐴)
79	72, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ⊆ ∪ 𝐴)
80		simpll3 1216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or ∪ 𝐴)
81		soss 5551	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏‘𝑗) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑗)))
82	79, 80, 81	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or (𝑏‘𝑗))
83		finnisoeu 10025	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 Or (𝑏‘𝑗) ∧ (𝑏‘𝑗) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
84	82, 73, 83	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))
85		iotacl 6477	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ V
88		isoeq1 7263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
89		isoeq1 7263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
90	89	cbvabv 2805	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))}
91	87, 88, 90	elab2 3636	. . . . . . . . . . . . . . . . . . . . . . . . 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 7269	. . . . . . . . . . . . . . . . . . . . . . . 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 6785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) → ^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗)))
96		f1of 6773	. . . . . . . . . . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ (𝑏‘𝑗))
101	97, 100	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)))
102	77, 101	sseldd 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω)
103		2fveq3 6838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑗 → (card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)))
104	103	eleq2d 2821	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑗 → (𝑔 ∈ (card‘(𝑏‘𝑓)) ↔ 𝑔 ∈ (card‘(𝑏‘𝑗))))
105		isoeq4 7266	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓))))
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓))))
107		fveq2 6833	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 = 𝑗 → (𝑏‘𝑓) = (𝑏‘𝑗))
108		isoeq5 7267	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑗 → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))))
112	111	fveq1d 6835	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑗 → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔))
113	104, 112	ifbieq1d 4503	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑗 → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) = if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎))
114		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → (𝑔 ∈ (card‘(𝑏‘𝑗)) ↔ (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗))))
115		fveq2 6833	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
116	114, 115	ifbieq1d 4503	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎) = if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎))
117		fvex 6846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) ∈ V
118		vex 3443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑎 ∈ V
119	117, 118	ifex 4529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) ∈ V
120	113, 116, 59, 119	ovmpo 7518	. . . . . . . . . . . . . . . . . . . . . 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 4486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → if((^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
123		f1ocnvfv2 7223	. . . . . . . . . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(^◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)))
126		rspceov 7407	. . . . . . . . . . . . . . . . . . . 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 3134	. . . . . . . . . . . . . . . 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 3126	. . . . . . . . . . 11 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))
136		foov 7532	. . . . . . . . . . 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 9969	. . . . . . . . . 10 ⊢ ((ω × ω) ∈ dom card → ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 → ∪ 𝐴 ≼ (ω × ω)))
139	25, 137, 138	mpsyl 68	. . . . . . . . 9 ⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) ∧ (𝑎 ∈ ∪ 𝐴 ∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ (ω × ω))
140		xpomen 9927	. . . . . . . . 9 ⊢ (ω × ω) ≈ ω
141		domentr 8952	. . . . . . . . 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 3014	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 2567 {cab 2713 ≠ wne 2931 ∀wral 3050 ∃wrex 3059 Vcvv 3439 ⊆ wss 3900 ∅c0 4284 ifcif 4478 ∪ cuni 4862 class class class wbr 5097 E cep 5522 Or wor 5530 × cxp 5621 ^◡ccnv 5622 dom cdm 5623 Ord word 6315 Oncon0 6316 ℩cio 6445 ⟶wf 6487 –onto→wfo 6489 –1-1-onto→wf1o 6490 ‘cfv 6491 Isom wiso 6492 (class class class)co 7358 ∈ cmpo 7360 ωcom 7808 ≈ cen 8882 ≼ cdom 8883 ≺ csdm 8884 Fincfn 8885 cardccrd 9849

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 2183 ax-ext 2707 ax-rep 5223 ax-sep 5240 ax-nul 5250 ax-pow 5309 ax-pr 5376 ax-un 7680 ax-inf2 9552

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 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-rmo 3349 df-reu 3350 df-rab 3399 df-v 3441 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4285 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4902 df-iun 4947 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6258 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6447 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-isom 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-oadd 8401 df-omul 8402 df-er 8635 df-map 8767 df-en 8886 df-dom 8887 df-sdom 8888 df-fin 8889 df-oi 9417 df-card 9853 df-acn 9856

This theorem is referenced by: aannenlem3 26296

W3C validator