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

Theorem cfsmolem 9293
Description: Lemma for cfsmo 9294. (Contributed by Mario Carneiro, 28-Feb-2013.)
Hypotheses
Ref Expression
cfsmolem.2 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ 𝑡 ∈ dom 𝑧 suc (𝑧𝑡)))
cfsmolem.3 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))
Assertion
Ref Expression
cfsmolem (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
Distinct variable groups:   𝑓,𝑔,𝑡,𝑤,𝑧,𝐴   𝑓,𝐹,𝑡,𝑧   𝑓,𝐺,𝑤,𝑧
Allowed substitution hints:   𝐹(𝑤,𝑔)   𝐺(𝑡,𝑔)

Proof of Theorem cfsmolem
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cff1 9281 . 2 (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)))
2 cfon 9278 . . . . . . . . . . . 12 (cf‘𝐴) ∈ On
32oneli 5978 . . . . . . . . . . 11 (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On)
433ad2ant3 1128 . . . . . . . . . 10 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
5 eleq1w 2832 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴)))
653anbi3d 1552 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴))))
7 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
87eleq1d 2834 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐺𝑥) ∈ 𝐴 ↔ (𝐺𝑦) ∈ 𝐴))
96, 8imbi12d 333 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴)))
10 simpl1 1226 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → 𝑔:(cf‘𝐴)–1-1𝐴)
11 simpl2 1228 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → 𝐴 ∈ On)
12 ontr1 5914 . . . . . . . . . . . . . . . . . 18 ((cf‘𝐴) ∈ On → ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)))
132, 12ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))
1413ancoms 455 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → 𝑦 ∈ (cf‘𝐴))
15143ad2antl3 1201 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → 𝑦 ∈ (cf‘𝐴))
16 pm2.27 42 . . . . . . . . . . . . . . 15 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴))
1710, 11, 15, 16syl3anc 1475 . . . . . . . . . . . . . 14 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴))
1817ralimdva 3110 . . . . . . . . . . . . 13 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴))
19 cfsmolem.3 . . . . . . . . . . . . . . . . . . . 20 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))
2019fveq1i 6333 . . . . . . . . . . . . . . . . . . 19 (𝐺𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥)
21 fvres 6348 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥))
2220, 21syl5eq 2816 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) = (recs(𝐹)‘𝑥))
23 recsval 7652 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥)))
24 recsfnon 7651 . . . . . . . . . . . . . . . . . . . . . . . 24 recs(𝐹) Fn On
25 fnfun 6128 . . . . . . . . . . . . . . . . . . . . . . . 24 (recs(𝐹) Fn On → Fun recs(𝐹))
2624, 25ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 Fun recs(𝐹)
27 vex 3352 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 ∈ V
28 resfunexg 6622 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V)
2926, 27, 28mp2an 664 . . . . . . . . . . . . . . . . . . . . . 22 (recs(𝐹) ↾ 𝑥) ∈ V
30 dmeq 5462 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥))
3130fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥)))
32 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡))
33 suceq 5933 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3432, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3530, 34iuneq12d 4678 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (recs(𝐹) ↾ 𝑥) → 𝑡 ∈ dom 𝑧 suc (𝑧𝑡) = 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3631, 35uneq12d 3917 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ 𝑡 ∈ dom 𝑧 suc (𝑧𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
37 cfsmolem.2 . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ 𝑡 ∈ dom 𝑧 suc (𝑧𝑡)))
38 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V
3929dmex 7245 . . . . . . . . . . . . . . . . . . . . . . . . 25 dom (recs(𝐹) ↾ 𝑥) ∈ V
40 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4140sucex 7157 . . . . . . . . . . . . . . . . . . . . . . . . 25 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4239, 41iunex 7293 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4338, 42unex 7102 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V
4436, 37, 43fvmpt 6424 . . . . . . . . . . . . . . . . . . . . . 22 ((recs(𝐹) ↾ 𝑥) ∈ V → (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
4529, 44ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
4623, 45syl6eq 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
47 onss 7136 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ On → 𝑥 ⊆ On)
48 fnssres 6144 . . . . . . . . . . . . . . . . . . . . . 22 ((recs(𝐹) Fn On ∧ 𝑥 ⊆ On) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
4924, 47, 48sylancr 567 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
50 fndm 6130 . . . . . . . . . . . . . . . . . . . . 21 ((recs(𝐹) ↾ 𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥)
51 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . 22 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔𝑥))
52 iuneq1 4666 . . . . . . . . . . . . . . . . . . . . . . 23 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
53 fvres 6348 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡))
54 suceq 5933 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
5553, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
5655iuneq2i 4671 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑡𝑥 suc (recs(𝐹)‘𝑡)
57 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡))
58 suceq 5933 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
6059cbviunv 4691 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝑡𝑥 suc (recs(𝐹)‘𝑡)
6156, 60eqtr4i 2795 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑦𝑥 suc (recs(𝐹)‘𝑦)
6252, 61syl6eq 2820 . . . . . . . . . . . . . . . . . . . . . 22 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑦𝑥 suc (recs(𝐹)‘𝑦))
6351, 62uneq12d 3917 . . . . . . . . . . . . . . . . . . . . 21 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
6449, 50, 633syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
6546, 64eqtrd 2804 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
663, 65syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
6722, 66eqtrd 2804 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
68673ad2ant2 1127 . . . . . . . . . . . . . . . 16 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐺𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
69 eloni 5876 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On → Ord 𝐴)
7069adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → Ord 𝐴)
71703ad2ant1 1126 . . . . . . . . . . . . . . . . 17 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → Ord 𝐴)
72 f1f 6241 . . . . . . . . . . . . . . . . . . . 20 (𝑔:(cf‘𝐴)–1-1𝐴𝑔:(cf‘𝐴)⟶𝐴)
7372ffvelrnda 6502 . . . . . . . . . . . . . . . . . . 19 ((𝑔:(cf‘𝐴)–1-1𝐴𝑥 ∈ (cf‘𝐴)) → (𝑔𝑥) ∈ 𝐴)
7473adantlr 686 . . . . . . . . . . . . . . . . . 18 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔𝑥) ∈ 𝐴)
75743adant3 1125 . . . . . . . . . . . . . . . . 17 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝑔𝑥) ∈ 𝐴)
7619fveq1i 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦)
7713fvresd 6349 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦))
7876, 77syl5eq 2816 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
7978adantrl 687 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
8079ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
8180eleq1d 2834 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴))
82 ordsucss 7164 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝐴 → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8369, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8483ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8581, 84sylbid 230 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8685ralimdva 3110 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
87 iunss 4693 . . . . . . . . . . . . . . . . . . . . 21 ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
8886, 87syl6ibr 242 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
89883impia 1108 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
90 onelon 5891 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On)
9190ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
9291ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
9381, 92sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
94 suceloni 7159 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On)
9593, 94syl6 35 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On))
9695ralimdva 3110 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On))
97963impia 1108 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
98 iunon 7588 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ V ∧ ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
9927, 98mpan 662 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
10097, 99syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
101 simp1 1129 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝐴 ∈ On)
102 onsseleq 5908 . . . . . . . . . . . . . . . . . . . . 21 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
103100, 101, 102syl2anc 565 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
104 idd 24 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
105 simpll 742 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝑥 ∈ (cf‘𝐴))
106 simprr 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝐴 ∈ On)
1073ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝑥 ∈ On)
1083, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (cf‘𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
109108adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
11078ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
111 fvres 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
112111adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
113110, 112eqtr4d 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → (𝐺𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
114113eleq1d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
115114ralbidva 3133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (cf‘𝐴) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 ↔ ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
116115biimpa 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
117 ffnfv 6530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((recs(𝐹) ↾ 𝑥):𝑥𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
118109, 116, 117sylanbrc 564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥𝐴)
119 eleq2 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡𝐴))
120119biimpar 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝑡𝐴) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
121120adantrl 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
1221213adant1 1123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
123 onelon 5891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐴 ∈ On ∧ 𝑡𝐴) → 𝑡 ∈ On)
124111adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
125 ffvelrn 6500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
126124, 125eqeltrrd 2850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴)
127126, 90sylan2 572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
128127adantlr 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
129 onsssuc 5956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
130123, 128, 129syl2an2r 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
131130anassrs 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) ∧ 𝑦𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
132131rexbidva 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
133 eliun 4656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))
134132, 133syl6bbr 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
135134ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
1361353adant2 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
137122, 136mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
1381373expa 1110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
139138anassrs 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡𝐴) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
140139ralrimiva 3114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
141140expl 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((recs(𝐹) ↾ 𝑥):𝑥𝐴 → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
142118, 141syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
143142imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
144 feq1 6166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥𝐴))
145 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
146145sseq2d 3780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
147146rexbidv 3199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
148111sseq2d 3780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦)))
149148rexbiia 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∃𝑦𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
150147, 149syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
151150ralbidv 3134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
152144, 151anbi12d 608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))))
15329, 152spcev 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)))
154118, 143, 153syl2an2r 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)))
155 cfflb 9282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)) → (cf‘𝐴) ⊆ 𝑥))
156155imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦))) → (cf‘𝐴) ⊆ 𝑥)
157106, 107, 154, 156syl21anc 1474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥)
158 ontri1 5900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((cf‘𝐴) ∈ On ∧ 𝑥 ∈ On) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
1592, 3, 158sylancr 567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
160159ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
161157, 160mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ¬ 𝑥 ∈ (cf‘𝐴))
162105, 161pm2.21dd 186 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
163162ex 397 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
164163expcomd 402 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐴 ∈ On → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
165164com12 32 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
1661653impib 1107 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
167104, 166jaod 839 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
168103, 167sylbid 230 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
16989, 168mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
1701693adant1l 1184 . . . . . . . . . . . . . . . . 17 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
171 ordunel 7173 . . . . . . . . . . . . . . . . 17 ((Ord 𝐴 ∧ (𝑔𝑥) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) → ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
17271, 75, 170, 171syl3anc 1475 . . . . . . . . . . . . . . . 16 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
17368, 172eqeltrd 2849 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐺𝑥) ∈ 𝐴)
1741733expia 1113 . . . . . . . . . . . . . 14 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → (𝐺𝑥) ∈ 𝐴))
1751743impa 1099 . . . . . . . . . . . . 13 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → (𝐺𝑥) ∈ 𝐴))
17618, 175syldc 48 . . . . . . . . . . . 12 (∀𝑦𝑥 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴))
177176a1i 11 . . . . . . . . . . 11 (𝑥 ∈ On → (∀𝑦𝑥 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴)))
1789, 177tfis2 7202 . . . . . . . . . 10 (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴))
1794, 178mpcom 38 . . . . . . . . 9 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴)
1801793expia 1113 . . . . . . . 8 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) ∈ 𝐴))
181180ralrimiv 3113 . . . . . . 7 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴)
1822onssi 7183 . . . . . . . . 9 (cf‘𝐴) ⊆ On
183 fnssres 6144 . . . . . . . . . 10 ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
18419fneq1i 6125 . . . . . . . . . 10 (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
185183, 184sylibr 224 . . . . . . . . 9 ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → 𝐺 Fn (cf‘𝐴))
18624, 182, 185mp2an 664 . . . . . . . 8 𝐺 Fn (cf‘𝐴)
187 ffnfv 6530 . . . . . . . 8 (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴))
188186, 187mpbiran 680 . . . . . . 7 (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴)
189181, 188sylibr 224 . . . . . 6 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
190189adantlr 686 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
191 onss 7136 . . . . . . . 8 (𝐴 ∈ On → 𝐴 ⊆ On)
192191adantl 467 . . . . . . 7 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → 𝐴 ⊆ On)
1932onordi 5975 . . . . . . . 8 Ord (cf‘𝐴)
194 fvex 6342 . . . . . . . . . . . . . . . . 17 (recs(𝐹)‘𝑦) ∈ V
195194sucid 5947 . . . . . . . . . . . . . . . 16 (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)
196 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦))
197 suceq 5933 . . . . . . . . . . . . . . . . . . 19 ((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
198196, 197syl 17 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
199198eliuni 4658 . . . . . . . . . . . . . . . . 17 ((𝑦𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ 𝑡𝑥 suc (recs(𝐹)‘𝑡))
200199, 60syl6eleqr 2860 . . . . . . . . . . . . . . . 16 ((𝑦𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
201195, 200mpan2 663 . . . . . . . . . . . . . . 15 (𝑦𝑥 → (recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
202 elun2 3930 . . . . . . . . . . . . . . 15 ((recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
203201, 202syl 17 . . . . . . . . . . . . . 14 (𝑦𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
204203adantr 466 . . . . . . . . . . . . 13 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
2053adantl 467 . . . . . . . . . . . . . 14 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
206205, 65syl 17 . . . . . . . . . . . . 13 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
207204, 206eleqtrrd 2852 . . . . . . . . . . . 12 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥))
20822adantl 467 . . . . . . . . . . . 12 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) = (recs(𝐹)‘𝑥))
209207, 78, 2083eltr4d 2864 . . . . . . . . . . 11 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ (𝐺𝑥))
210209expcom 398 . . . . . . . . . 10 (𝑥 ∈ (cf‘𝐴) → (𝑦𝑥 → (𝐺𝑦) ∈ (𝐺𝑥)))
211210ralrimiv 3113 . . . . . . . . 9 (𝑥 ∈ (cf‘𝐴) → ∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥))
212211rgen 3070 . . . . . . . 8 𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)
213 issmo2 7598 . . . . . . . . 9 (𝐺:(cf‘𝐴)⟶𝐴 → ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)) → Smo 𝐺))
214213com12 32 . . . . . . . 8 ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)) → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
215193, 212, 214mp3an23 1563 . . . . . . 7 (𝐴 ⊆ On → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
216192, 189, 215sylc 65 . . . . . 6 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → Smo 𝐺)
217216adantlr 686 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → Smo 𝐺)
218 fveq2 6332 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑔𝑥) = (𝑔𝑤))
219 fveq2 6332 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
220218, 219sseq12d 3781 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑔𝑥) ⊆ (𝐺𝑥) ↔ (𝑔𝑤) ⊆ (𝐺𝑤)))
221 ssun1 3925 . . . . . . . . . . 11 (𝑔𝑥) ⊆ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
222221, 67syl5sseqr 3801 . . . . . . . . . 10 (𝑥 ∈ (cf‘𝐴) → (𝑔𝑥) ⊆ (𝐺𝑥))
223220, 222vtoclga 3421 . . . . . . . . 9 (𝑤 ∈ (cf‘𝐴) → (𝑔𝑤) ⊆ (𝐺𝑤))
224 sstr 3758 . . . . . . . . . 10 ((𝑧 ⊆ (𝑔𝑤) ∧ (𝑔𝑤) ⊆ (𝐺𝑤)) → 𝑧 ⊆ (𝐺𝑤))
225224expcom 398 . . . . . . . . 9 ((𝑔𝑤) ⊆ (𝐺𝑤) → (𝑧 ⊆ (𝑔𝑤) → 𝑧 ⊆ (𝐺𝑤)))
226223, 225syl 17 . . . . . . . 8 (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔𝑤) → 𝑧 ⊆ (𝐺𝑤)))
227226reximia 3156 . . . . . . 7 (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
228227ralimi 3100 . . . . . 6 (∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤) → ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
229228ad2antlr 698 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
230 fnex 6624 . . . . . . 7 ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V)
231186, 2, 230mp2an 664 . . . . . 6 𝐺 ∈ V
232 feq1 6166 . . . . . . 7 (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴𝐺:(cf‘𝐴)⟶𝐴))
233 smoeq 7599 . . . . . . 7 (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺))
234 fveq1 6331 . . . . . . . . . 10 (𝑓 = 𝐺 → (𝑓𝑤) = (𝐺𝑤))
235234sseq2d 3780 . . . . . . . . 9 (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓𝑤) ↔ 𝑧 ⊆ (𝐺𝑤)))
236235rexbidv 3199 . . . . . . . 8 (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)))
237236ralbidv 3134 . . . . . . 7 (𝑓 = 𝐺 → (∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤) ↔ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)))
238232, 233, 2373anbi123d 1546 . . . . . 6 (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))))
239231, 238spcev 3449 . . . . 5 ((𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
240190, 217, 229, 239syl3anc 1475 . . . 4 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
241240expcom 398 . . 3 (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤))))
242241exlimdv 2012 . 2 (𝐴 ∈ On → (∃𝑔(𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤))))
2431, 242mpd 15 1 (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826  w3a 1070   = wceq 1630  wex 1851  wcel 2144  wral 3060  wrex 3061  Vcvv 3349  cun 3719  wss 3721   ciun 4652  cmpt 4861  dom cdm 5249  cres 5251  Ord word 5865  Oncon0 5866  suc csuc 5868  Fun wfun 6025   Fn wfn 6026  wf 6027  1-1wf1 6028  cfv 6031  Smo wsmo 7594  recscrecs 7619  cfccf 8962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-smo 7595  df-recs 7620  df-er 7895  df-map 8010  df-en 8109  df-dom 8110  df-sdom 8111  df-card 8964  df-cf 8966  df-acn 8967
This theorem is referenced by:  cfsmo  9294
  Copyright terms: Public domain W3C validator