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

Theorem cfsmolem 9089
Description: Lemma for cfsmo 9090. (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 9077 . 2 (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)))
2 cfon 9074 . . . . . . . . . . . 12 (cf‘𝐴) ∈ On
32oneli 5833 . . . . . . . . . . 11 (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On)
433ad2ant3 1083 . . . . . . . . . 10 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
5 eleq1 2688 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴)))
653anbi3d 1404 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴))))
7 fveq2 6189 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
87eleq1d 2685 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐺𝑥) ∈ 𝐴 ↔ (𝐺𝑦) ∈ 𝐴))
96, 8imbi12d 334 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴)))
10 simpl1 1063 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → 𝑔:(cf‘𝐴)–1-1𝐴)
11 simpl2 1064 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → 𝐴 ∈ On)
12 ontr1 5769 . . . . . . . . . . . . . . . . . 18 ((cf‘𝐴) ∈ On → ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)))
132, 12ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))
1413ancoms 469 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → 𝑦 ∈ (cf‘𝐴))
15143ad2antl3 1224 . . . . . . . . . . . . . . 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 1325 . . . . . . . . . . . . . 14 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴))
1817ralimdva 2961 . . . . . . . . . . . . 13 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴))
19 cfsmolem.3 . . . . . . . . . . . . . . . . . . . 20 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))
2019fveq1i 6190 . . . . . . . . . . . . . . . . . . 19 (𝐺𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥)
21 fvres 6205 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥))
2220, 21syl5eq 2667 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) = (recs(𝐹)‘𝑥))
23 recsval 7497 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥)))
24 recsfnon 7496 . . . . . . . . . . . . . . . . . . . . . . . 24 recs(𝐹) Fn On
25 fnfun 5986 . . . . . . . . . . . . . . . . . . . . . . . 24 (recs(𝐹) Fn On → Fun recs(𝐹))
2624, 25ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 Fun recs(𝐹)
27 vex 3201 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 ∈ V
28 resfunexg 6476 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V)
2926, 27, 28mp2an 708 . . . . . . . . . . . . . . . . . . . . . 22 (recs(𝐹) ↾ 𝑥) ∈ V
30 dmeq 5322 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥))
3130fveq2d 6193 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥)))
32 fveq1 6188 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡))
33 suceq 5788 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3432, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3530, 34iuneq12d 4544 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (recs(𝐹) ↾ 𝑥) → 𝑡 ∈ dom 𝑧 suc (𝑧𝑡) = 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3631, 35uneq12d 3766 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ 𝑡 ∈ dom 𝑧 suc (𝑧𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
37 cfsmolem.2 . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ 𝑡 ∈ dom 𝑧 suc (𝑧𝑡)))
38 fvex 6199 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V
3929dmex 7096 . . . . . . . . . . . . . . . . . . . . . . . . 25 dom (recs(𝐹) ↾ 𝑥) ∈ V
40 fvex 6199 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4140sucex 7008 . . . . . . . . . . . . . . . . . . . . . . . . 25 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4239, 41iunex 7144 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4338, 42unex 6953 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V
4436, 37, 43fvmpt 6280 . . . . . . . . . . . . . . . . . . . . . 22 ((recs(𝐹) ↾ 𝑥) ∈ V → (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
4529, 44ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
4623, 45syl6eq 2671 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
47 onss 6987 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ On → 𝑥 ⊆ On)
48 fnssres 6002 . . . . . . . . . . . . . . . . . . . . . 22 ((recs(𝐹) Fn On ∧ 𝑥 ⊆ On) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
4924, 47, 48sylancr 695 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
50 fndm 5988 . . . . . . . . . . . . . . . . . . . . 21 ((recs(𝐹) ↾ 𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥)
51 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . 22 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔𝑥))
52 iuneq1 4532 . . . . . . . . . . . . . . . . . . . . . . 23 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
53 fvres 6205 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡))
54 suceq 5788 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
5553, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
5655iuneq2i 4537 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑡𝑥 suc (recs(𝐹)‘𝑡)
57 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡))
58 suceq 5788 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
6059cbviunv 4557 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝑡𝑥 suc (recs(𝐹)‘𝑡)
6156, 60eqtr4i 2646 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑦𝑥 suc (recs(𝐹)‘𝑦)
6252, 61syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . 22 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑦𝑥 suc (recs(𝐹)‘𝑦))
6351, 62uneq12d 3766 . . . . . . . . . . . . . . . . . . . . 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 2655 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
663, 65syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
6722, 66eqtrd 2655 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
68673ad2ant2 1082 . . . . . . . . . . . . . . . 16 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐺𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
69 eloni 5731 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ On → Ord 𝐴)
7069adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → Ord 𝐴)
71703ad2ant1 1081 . . . . . . . . . . . . . . . . 17 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → Ord 𝐴)
72 f1f 6099 . . . . . . . . . . . . . . . . . . . 20 (𝑔:(cf‘𝐴)–1-1𝐴𝑔:(cf‘𝐴)⟶𝐴)
7372ffvelrnda 6357 . . . . . . . . . . . . . . . . . . 19 ((𝑔:(cf‘𝐴)–1-1𝐴𝑥 ∈ (cf‘𝐴)) → (𝑔𝑥) ∈ 𝐴)
7473adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔𝑥) ∈ 𝐴)
75743adant3 1080 . . . . . . . . . . . . . . . . 17 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝑔𝑥) ∈ 𝐴)
7619fveq1i 6190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦)
7713fvresd 6206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦))
7876, 77syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
7978adantrl 752 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
8079ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
8180eleq1d 2685 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴))
82 ordsucss 7015 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝐴 → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8369, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8483ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8581, 84sylbid 230 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8685ralimdva 2961 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
87 iunss 4559 . . . . . . . . . . . . . . . . . . . . 21 ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
8886, 87syl6ibr 242 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
89883impia 1260 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
90 onelon 5746 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On)
9190ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
9291ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
9381, 92sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
94 suceloni 7010 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On)
9593, 94syl6 35 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On))
9695ralimdva 2961 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On))
97963impia 1260 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
98 iunon 7433 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ V ∧ ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
9927, 98mpan 706 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
10097, 99syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
101 simp1 1060 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝐴 ∈ On)
102 onsseleq 5763 . . . . . . . . . . . . . . . . . . . . 21 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
103100, 101, 102syl2anc 693 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
104 idd 24 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
105 simpll 790 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝑥 ∈ (cf‘𝐴))
106 simprr 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝐴 ∈ On)
1073ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝑥 ∈ On)
1083, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (cf‘𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
109108adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
11078ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
111 fvres 6205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
112111adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
113110, 112eqtr4d 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → (𝐺𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
114113eleq1d 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
115114ralbidva 2984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (cf‘𝐴) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 ↔ ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
116115biimpa 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
117 ffnfv 6386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((recs(𝐹) ↾ 𝑥):𝑥𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
118109, 116, 117sylanbrc 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥𝐴)
119 eleq2 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡𝐴))
120119biimpar 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝑡𝐴) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
121120adantrl 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
1221213adant1 1078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
123 onelon 5746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐴 ∈ On ∧ 𝑡𝐴) → 𝑡 ∈ On)
124111adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
125 ffvelrn 6355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
126124, 125eqeltrrd 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴)
127126, 90sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
128127adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
129 onsssuc 5811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
130123, 128, 129syl2an2r 876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
131130anassrs 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) ∧ 𝑦𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
132131rexbidva 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
133 eliun 4522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))
134132, 133syl6bbr 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
135134ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
1361353adant2 1079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
137122, 136mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
1381373expa 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
139138anassrs 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡𝐴) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
140139ralrimiva 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
141140expl 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((recs(𝐹) ↾ 𝑥):𝑥𝐴 → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
142118, 141syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
143142imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
144 feq1 6024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥𝐴))
145 fveq1 6188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
146145sseq2d 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
147146rexbidv 3050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
148111sseq2d 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦)))
149148rexbiia 3038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∃𝑦𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
150147, 149syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
151150ralbidv 2985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
152144, 151anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))))
15329, 152spcev 3298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)))
154118, 143, 153syl2an2r 876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)))
155 cfflb 9078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)) → (cf‘𝐴) ⊆ 𝑥))
156155imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦))) → (cf‘𝐴) ⊆ 𝑥)
157106, 107, 154, 156syl21anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥)
158 ontri1 5755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((cf‘𝐴) ∈ On ∧ 𝑥 ∈ On) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
1592, 3, 158sylancr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
160159ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 450 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
164163expcomd 454 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐴 ∈ On → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
165164com12 32 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
1661653impib 1261 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
167104, 166jaod 395 . . . . . . . . . . . . . . . . . . . 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 1317 . . . . . . . . . . . . . . . . 17 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
171 ordunel 7024 . . . . . . . . . . . . . . . . 17 ((Ord 𝐴 ∧ (𝑔𝑥) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) → ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
17271, 75, 170, 171syl3anc 1325 . . . . . . . . . . . . . . . 16 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
17368, 172eqeltrd 2700 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐺𝑥) ∈ 𝐴)
1741733expia 1266 . . . . . . . . . . . . . 14 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → (𝐺𝑥) ∈ 𝐴))
1751743impa 1258 . . . . . . . . . . . . 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 7053 . . . . . . . . . 10 (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴))
1794, 178mpcom 38 . . . . . . . . 9 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴)
1801793expia 1266 . . . . . . . 8 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) ∈ 𝐴))
181180ralrimiv 2964 . . . . . . 7 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴)
1822onssi 7034 . . . . . . . . 9 (cf‘𝐴) ⊆ On
183 fnssres 6002 . . . . . . . . . 10 ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
18419fneq1i 5983 . . . . . . . . . 10 (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
185183, 184sylibr 224 . . . . . . . . 9 ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → 𝐺 Fn (cf‘𝐴))
18624, 182, 185mp2an 708 . . . . . . . 8 𝐺 Fn (cf‘𝐴)
187 ffnfv 6386 . . . . . . . 8 (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴))
188186, 187mpbiran 953 . . . . . . 7 (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴)
189181, 188sylibr 224 . . . . . 6 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
190189adantlr 751 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
191 onss 6987 . . . . . . . 8 (𝐴 ∈ On → 𝐴 ⊆ On)
192191adantl 482 . . . . . . 7 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → 𝐴 ⊆ On)
1932onordi 5830 . . . . . . . 8 Ord (cf‘𝐴)
194 fvex 6199 . . . . . . . . . . . . . . . . 17 (recs(𝐹)‘𝑦) ∈ V
195194sucid 5802 . . . . . . . . . . . . . . . 16 (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)
196 fveq2 6189 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦))
197 suceq 5788 . . . . . . . . . . . . . . . . . . 19 ((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
198196, 197syl 17 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
199198eliuni 4524 . . . . . . . . . . . . . . . . 17 ((𝑦𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ 𝑡𝑥 suc (recs(𝐹)‘𝑡))
200199, 60syl6eleqr 2711 . . . . . . . . . . . . . . . 16 ((𝑦𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
201195, 200mpan2 707 . . . . . . . . . . . . . . 15 (𝑦𝑥 → (recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
202 elun2 3779 . . . . . . . . . . . . . . 15 ((recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
203201, 202syl 17 . . . . . . . . . . . . . 14 (𝑦𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
204203adantr 481 . . . . . . . . . . . . 13 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
2053adantl 482 . . . . . . . . . . . . . 14 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
206205, 65syl 17 . . . . . . . . . . . . 13 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
207204, 206eleqtrrd 2703 . . . . . . . . . . . 12 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥))
20822adantl 482 . . . . . . . . . . . 12 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) = (recs(𝐹)‘𝑥))
209207, 78, 2083eltr4d 2715 . . . . . . . . . . 11 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ (𝐺𝑥))
210209expcom 451 . . . . . . . . . 10 (𝑥 ∈ (cf‘𝐴) → (𝑦𝑥 → (𝐺𝑦) ∈ (𝐺𝑥)))
211210ralrimiv 2964 . . . . . . . . 9 (𝑥 ∈ (cf‘𝐴) → ∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥))
212211rgen 2921 . . . . . . . 8 𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)
213 issmo2 7443 . . . . . . . . 9 (𝐺:(cf‘𝐴)⟶𝐴 → ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)) → Smo 𝐺))
214213com12 32 . . . . . . . 8 ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)) → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
215193, 212, 214mp3an23 1415 . . . . . . 7 (𝐴 ⊆ On → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
216192, 189, 215sylc 65 . . . . . 6 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → Smo 𝐺)
217216adantlr 751 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → Smo 𝐺)
218 fveq2 6189 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑔𝑥) = (𝑔𝑤))
219 fveq2 6189 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
220218, 219sseq12d 3632 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑔𝑥) ⊆ (𝐺𝑥) ↔ (𝑔𝑤) ⊆ (𝐺𝑤)))
221 ssun1 3774 . . . . . . . . . . 11 (𝑔𝑥) ⊆ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
222221, 67syl5sseqr 3652 . . . . . . . . . 10 (𝑥 ∈ (cf‘𝐴) → (𝑔𝑥) ⊆ (𝐺𝑥))
223220, 222vtoclga 3270 . . . . . . . . 9 (𝑤 ∈ (cf‘𝐴) → (𝑔𝑤) ⊆ (𝐺𝑤))
224 sstr 3609 . . . . . . . . . 10 ((𝑧 ⊆ (𝑔𝑤) ∧ (𝑔𝑤) ⊆ (𝐺𝑤)) → 𝑧 ⊆ (𝐺𝑤))
225224expcom 451 . . . . . . . . 9 ((𝑔𝑤) ⊆ (𝐺𝑤) → (𝑧 ⊆ (𝑔𝑤) → 𝑧 ⊆ (𝐺𝑤)))
226223, 225syl 17 . . . . . . . 8 (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔𝑤) → 𝑧 ⊆ (𝐺𝑤)))
227226reximia 3008 . . . . . . 7 (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
228227ralimi 2951 . . . . . 6 (∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤) → ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
229228ad2antlr 763 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
230 fnex 6478 . . . . . . 7 ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V)
231186, 2, 230mp2an 708 . . . . . 6 𝐺 ∈ V
232 feq1 6024 . . . . . . 7 (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴𝐺:(cf‘𝐴)⟶𝐴))
233 smoeq 7444 . . . . . . 7 (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺))
234 fveq1 6188 . . . . . . . . . 10 (𝑓 = 𝐺 → (𝑓𝑤) = (𝐺𝑤))
235234sseq2d 3631 . . . . . . . . 9 (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓𝑤) ↔ 𝑧 ⊆ (𝐺𝑤)))
236235rexbidv 3050 . . . . . . . 8 (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)))
237236ralbidv 2985 . . . . . . 7 (𝑓 = 𝐺 → (∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤) ↔ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)))
238232, 233, 2373anbi123d 1398 . . . . . 6 (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))))
239231, 238spcev 3298 . . . . 5 ((𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
240190, 217, 229, 239syl3anc 1325 . . . 4 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
241240expcom 451 . . 3 (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤))))
242241exlimdv 1860 . 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  wo 383  wa 384  w3a 1037   = wceq 1482  wex 1703  wcel 1989  wral 2911  wrex 2912  Vcvv 3198  cun 3570  wss 3572   ciun 4518  cmpt 4727  dom cdm 5112  cres 5114  Ord word 5720  Oncon0 5721  suc csuc 5723  Fun wfun 5880   Fn wfn 5881  wf 5882  1-1wf1 5883  cfv 5886  Smo wsmo 7439  recscrecs 7464  cfccf 8760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-smo 7440  df-recs 7465  df-er 7739  df-map 7856  df-en 7953  df-dom 7954  df-sdom 7955  df-card 8762  df-cf 8764  df-acn 8765
This theorem is referenced by:  cfsmo  9090
  Copyright terms: Public domain W3C validator