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

Theorem cfsmolem 8975
Description: Lemma for cfsmo 8976. (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 8963 . 2 (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)))
2 cfon 8960 . . . . . . . . . . . 12 (cf‘𝐴) ∈ On
32oneli 5752 . . . . . . . . . . 11 (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On)
433ad2ant3 1077 . . . . . . . . . 10 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
5 eleq1 2676 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴)))
653anbi3d 1397 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴))))
7 fveq2 6103 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
87eleq1d 2672 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐺𝑥) ∈ 𝐴 ↔ (𝐺𝑦) ∈ 𝐴))
96, 8imbi12d 333 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴)))
10 simpl1 1057 . . . . . . . . . . . . . . . 16 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → 𝑔:(cf‘𝐴)–1-1𝐴)
11 simpl2 1058 . . . . . . . . . . . . . . . 16 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → 𝐴 ∈ On)
12 ontr1 5688 . . . . . . . . . . . . . . . . . . 19 ((cf‘𝐴) ∈ On → ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)))
132, 12ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))
1413ancoms 468 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → 𝑦 ∈ (cf‘𝐴))
15143ad2antl3 1218 . . . . . . . . . . . . . . . 16 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → 𝑦 ∈ (cf‘𝐴))
16 pm2.27 41 . . . . . . . . . . . . . . . 16 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴))
1710, 11, 15, 16syl3anc 1318 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → (𝐺𝑦) ∈ 𝐴))
1817ralimdva 2945 . . . . . . . . . . . . . 14 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴))
19 cfsmolem.3 . . . . . . . . . . . . . . . . . . . . 21 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))
2019fveq1i 6104 . . . . . . . . . . . . . . . . . . . 20 (𝐺𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥)
21 fvres 6117 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥))
2220, 21syl5eq 2656 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) = (recs(𝐹)‘𝑥))
23 recsval 7387 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥)))
24 recsfnon 7386 . . . . . . . . . . . . . . . . . . . . . . . . 25 recs(𝐹) Fn On
25 fnfun 5902 . . . . . . . . . . . . . . . . . . . . . . . . 25 (recs(𝐹) Fn On → Fun recs(𝐹))
2624, 25ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 Fun recs(𝐹)
27 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 ∈ V
28 resfunexg 6384 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Fun recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V)
2926, 27, 28mp2an 704 . . . . . . . . . . . . . . . . . . . . . . 23 (recs(𝐹) ↾ 𝑥) ∈ V
30 dmeq 5246 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥))
3130fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥)))
32 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡))
33 suceq 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3432, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3530, 34iuneq12d 4482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (recs(𝐹) ↾ 𝑥) → 𝑡 ∈ dom 𝑧 suc (𝑧𝑡) = 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
3631, 35uneq12d 3730 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ 𝑡 ∈ dom 𝑧 suc (𝑧𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
37 cfsmolem.2 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ 𝑡 ∈ dom 𝑧 suc (𝑧𝑡)))
38 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V
3929dmex 6991 . . . . . . . . . . . . . . . . . . . . . . . . . 26 dom (recs(𝐹) ↾ 𝑥) ∈ V
40 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4140sucex 6903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4239, 41iunex 7039 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V
4338, 42unex 6854 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V
4436, 37, 43fvmpt 6191 . . . . . . . . . . . . . . . . . . . . . . 23 ((recs(𝐹) ↾ 𝑥) ∈ V → (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
4529, 44ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
4623, 45syl6eq 2660 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)))
47 onss 6882 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ On → 𝑥 ⊆ On)
48 fnssres 5918 . . . . . . . . . . . . . . . . . . . . . . 23 ((recs(𝐹) Fn On ∧ 𝑥 ⊆ On) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
4924, 47, 48sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
50 fndm 5904 . . . . . . . . . . . . . . . . . . . . . 22 ((recs(𝐹) ↾ 𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥)
51 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔𝑥))
52 iuneq1 4470 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡))
53 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡))
54 suceq 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
5553, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡))
5655iuneq2i 4475 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑡𝑥 suc (recs(𝐹)‘𝑡)
57 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡))
58 suceq 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡))
6059cbviunv 4495 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝑡𝑥 suc (recs(𝐹)‘𝑡)
6156, 60eqtr4i 2635 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑦𝑥 suc (recs(𝐹)‘𝑦)
6252, 61syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . 23 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = 𝑦𝑥 suc (recs(𝐹)‘𝑦))
6351, 62uneq12d 3730 . . . . . . . . . . . . . . . . . . . . . 22 (dom (recs(𝐹) ↾ 𝑥) = 𝑥 → ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
6449, 50, 633syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ On → ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
6546, 64eqtrd 2644 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
663, 65syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
6722, 66eqtrd 2644 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
68673ad2ant2 1076 . . . . . . . . . . . . . . . . 17 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐺𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
69 eloni 5650 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ On → Ord 𝐴)
7069adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → Ord 𝐴)
71703ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → Ord 𝐴)
72 f1f 6014 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:(cf‘𝐴)–1-1𝐴𝑔:(cf‘𝐴)⟶𝐴)
7372ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:(cf‘𝐴)–1-1𝐴𝑥 ∈ (cf‘𝐴)) → (𝑔𝑥) ∈ 𝐴)
7473adantlr 747 . . . . . . . . . . . . . . . . . . 19 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔𝑥) ∈ 𝐴)
75743adant3 1074 . . . . . . . . . . . . . . . . . 18 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝑔𝑥) ∈ 𝐴)
7619fveq1i 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐺𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦)
7713fvresd 6118 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦))
7876, 77syl5eq 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
7978adantrl 748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
8079ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
8180eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴))
82 ordsucss 6910 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord 𝐴 → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8369, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8483ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8581, 84sylbid 229 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
8685ralimdva 2945 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
87 iunss 4497 . . . . . . . . . . . . . . . . . . . . . 22 ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
8886, 87syl6ibr 241 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴))
89883impia 1253 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)
90 onelon 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On)
9190ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
9291ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
9381, 92sylbid 229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On))
94 suceloni 6905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On)
9593, 94syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On))
9695ralimdva 2945 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On))
97963impia 1253 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
98 iunon 7323 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ V ∧ ∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
9927, 98mpan 702 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
10097, 99syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On)
101 simp1 1054 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝐴 ∈ On)
102 onsseleq 5682 . . . . . . . . . . . . . . . . . . . . . 22 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
103100, 101, 102syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴)))
104 idd 24 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
105 simpll 786 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝑥 ∈ (cf‘𝐴))
106 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝐴 ∈ On)
1073ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝑥 ∈ On)
1083, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (cf‘𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
109108adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥)
11078ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → (𝐺𝑦) = (recs(𝐹)‘𝑦))
111 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
112111adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
113110, 112eqtr4d 2647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → (𝐺𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
114113eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦𝑥) → ((𝐺𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
115114ralbidva 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (cf‘𝐴) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 ↔ ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
116115biimpa 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
117 ffnfv 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((recs(𝐹) ↾ 𝑥):𝑥𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴))
118109, 116, 117sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥𝐴)
119 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡𝐴))
120119biimpar 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝑡𝐴) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
121120adantrl 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
1221213adant1 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦))
123 onelon 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐴 ∈ On ∧ 𝑡𝐴) → 𝑡 ∈ On)
124111adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦))
125 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)
126124, 125eqeltrrd 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴)
127126, 90sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
128127adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (recs(𝐹)‘𝑦) ∈ On)
129 onsssuc 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
130123, 128, 129syl2an2r 872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥𝐴𝑦𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
131130anassrs 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) ∧ 𝑦𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
132131rexbidva 3031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)))
133 eliun 4460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))
134132, 133syl6bbr 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝐴 ∈ On ∧ 𝑡𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥𝐴) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
135134ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
1361353adant2 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → (∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
137122, 136mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
1381373expa 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡𝐴)) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
139138anassrs 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡𝐴) → ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
140139ralrimiva 2949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((recs(𝐹) ↾ 𝑥):𝑥𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
141140expl 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((recs(𝐹) ↾ 𝑥):𝑥𝐴 → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
142118, 141syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
143142imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
144 feq1 5939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥𝐴))
145 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦))
146145sseq2d 3596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
147146rexbidv 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦)))
148111sseq2d 3596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦)))
149148rexbiia 3022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑦𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))
150147, 149syl6bb 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∃𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
151150ralbidv 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦) ↔ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))
152144, 151anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))))
15329, 152spcev 3273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((recs(𝐹) ↾ 𝑥):𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)))
154118, 143, 153syl2an2r 872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)))
155 cfflb 8964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦)) → (cf‘𝐴) ⊆ 𝑥))
156155imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥𝐴 ∧ ∀𝑡𝐴𝑦𝑥 𝑡 ⊆ (𝑓𝑦))) → (cf‘𝐴) ⊆ 𝑥)
157106, 107, 154, 156syl21anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥)
158 ontri1 5674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((cf‘𝐴) ∈ On ∧ 𝑥 ∈ On) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
1592, 3, 158sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
160159ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴)))
161157, 160mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → ¬ 𝑥 ∈ (cf‘𝐴))
162105, 161pm2.21dd 185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) ∧ ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On)) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
163162ex 449 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴𝐴 ∈ On) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
164163expcomd 453 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐴 ∈ On → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
165164com12 32 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)))
1661653impib 1254 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
167104, 166jaod 394 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
168103, 167sylbid 229 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ( 𝑦𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))
16989, 168mpd 15 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
1701693adant1l 1310 . . . . . . . . . . . . . . . . . 18 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)
171 ordunel 6919 . . . . . . . . . . . . . . . . . 18 ((Ord 𝐴 ∧ (𝑔𝑥) ∈ 𝐴 𝑦𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) → ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
17271, 75, 170, 171syl3anc 1318 . . . . . . . . . . . . . . . . 17 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴)
17368, 172eqeltrd 2688 . . . . . . . . . . . . . . . 16 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴) → (𝐺𝑥) ∈ 𝐴)
1741733expia 1259 . . . . . . . . . . . . . . 15 (((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → (𝐺𝑥) ∈ 𝐴))
1751743impa 1251 . . . . . . . . . . . . . 14 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 (𝐺𝑦) ∈ 𝐴 → (𝐺𝑥) ∈ 𝐴))
17618, 175syld 46 . . . . . . . . . . . . 13 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦𝑥 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → (𝐺𝑥) ∈ 𝐴))
177176com12 32 . . . . . . . . . . . 12 (∀𝑦𝑥 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴))
178177a1i 11 . . . . . . . . . . 11 (𝑥 ∈ On → (∀𝑦𝑥 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴)))
1799, 178tfis2 6948 . . . . . . . . . 10 (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴))
1804, 179mpcom 37 . . . . . . . . 9 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) ∈ 𝐴)
1811803expia 1259 . . . . . . . 8 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺𝑥) ∈ 𝐴))
182181ralrimiv 2948 . . . . . . 7 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴)
1832onssi 6929 . . . . . . . . 9 (cf‘𝐴) ⊆ On
184 fnssres 5918 . . . . . . . . . 10 ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
18519fneq1i 5899 . . . . . . . . . 10 (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴))
186184, 185sylibr 223 . . . . . . . . 9 ((recs(𝐹) Fn On ∧ (cf‘𝐴) ⊆ On) → 𝐺 Fn (cf‘𝐴))
18724, 183, 186mp2an 704 . . . . . . . 8 𝐺 Fn (cf‘𝐴)
188 ffnfv 6295 . . . . . . . 8 (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴))
189187, 188mpbiran 955 . . . . . . 7 (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺𝑥) ∈ 𝐴)
190182, 189sylibr 223 . . . . . 6 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
191190adantlr 747 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴)
192 onss 6882 . . . . . . . 8 (𝐴 ∈ On → 𝐴 ⊆ On)
193192adantl 481 . . . . . . 7 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → 𝐴 ⊆ On)
1942onordi 5749 . . . . . . . 8 Ord (cf‘𝐴)
195 fvex 6113 . . . . . . . . . . . . . . . . 17 (recs(𝐹)‘𝑦) ∈ V
196195sucid 5721 . . . . . . . . . . . . . . . 16 (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)
197 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦))
198 suceq 5707 . . . . . . . . . . . . . . . . . . 19 ((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
199197, 198syl 17 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦))
200199eliuni 4462 . . . . . . . . . . . . . . . . 17 ((𝑦𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ 𝑡𝑥 suc (recs(𝐹)‘𝑡))
201200, 60syl6eleqr 2699 . . . . . . . . . . . . . . . 16 ((𝑦𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
202196, 201mpan2 703 . . . . . . . . . . . . . . 15 (𝑦𝑥 → (recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
203 elun2 3743 . . . . . . . . . . . . . . 15 ((recs(𝐹)‘𝑦) ∈ 𝑦𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
204202, 203syl 17 . . . . . . . . . . . . . 14 (𝑦𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
205204adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
2063adantl 481 . . . . . . . . . . . . . 14 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On)
207206, 65syl 17 . . . . . . . . . . . . 13 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦)))
208205, 207eleqtrrd 2691 . . . . . . . . . . . 12 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥))
20922adantl 481 . . . . . . . . . . . 12 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑥) = (recs(𝐹)‘𝑥))
210208, 78, 2093eltr4d 2703 . . . . . . . . . . 11 ((𝑦𝑥𝑥 ∈ (cf‘𝐴)) → (𝐺𝑦) ∈ (𝐺𝑥))
211210expcom 450 . . . . . . . . . 10 (𝑥 ∈ (cf‘𝐴) → (𝑦𝑥 → (𝐺𝑦) ∈ (𝐺𝑥)))
212211ralrimiv 2948 . . . . . . . . 9 (𝑥 ∈ (cf‘𝐴) → ∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥))
213212rgen 2906 . . . . . . . 8 𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)
214 issmo2 7333 . . . . . . . . 9 (𝐺:(cf‘𝐴)⟶𝐴 → ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)) → Smo 𝐺))
215214com12 32 . . . . . . . 8 ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦𝑥 (𝐺𝑦) ∈ (𝐺𝑥)) → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
216194, 213, 215mp3an23 1408 . . . . . . 7 (𝐴 ⊆ On → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺))
217193, 190, 216sylc 63 . . . . . 6 ((𝑔:(cf‘𝐴)–1-1𝐴𝐴 ∈ On) → Smo 𝐺)
218217adantlr 747 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → Smo 𝐺)
219 fveq2 6103 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑔𝑥) = (𝑔𝑤))
220 fveq2 6103 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
221219, 220sseq12d 3597 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝑔𝑥) ⊆ (𝐺𝑥) ↔ (𝑔𝑤) ⊆ (𝐺𝑤)))
222 ssun1 3738 . . . . . . . . . . 11 (𝑔𝑥) ⊆ ((𝑔𝑥) ∪ 𝑦𝑥 suc (recs(𝐹)‘𝑦))
223222, 67syl5sseqr 3617 . . . . . . . . . 10 (𝑥 ∈ (cf‘𝐴) → (𝑔𝑥) ⊆ (𝐺𝑥))
224221, 223vtoclga 3245 . . . . . . . . 9 (𝑤 ∈ (cf‘𝐴) → (𝑔𝑤) ⊆ (𝐺𝑤))
225 sstr 3576 . . . . . . . . . 10 ((𝑧 ⊆ (𝑔𝑤) ∧ (𝑔𝑤) ⊆ (𝐺𝑤)) → 𝑧 ⊆ (𝐺𝑤))
226225expcom 450 . . . . . . . . 9 ((𝑔𝑤) ⊆ (𝐺𝑤) → (𝑧 ⊆ (𝑔𝑤) → 𝑧 ⊆ (𝐺𝑤)))
227224, 226syl 17 . . . . . . . 8 (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔𝑤) → 𝑧 ⊆ (𝐺𝑤)))
228227reximia 2992 . . . . . . 7 (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
229228ralimi 2936 . . . . . 6 (∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤) → ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
230229ad2antlr 759 . . . . 5 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))
231 fnex 6386 . . . . . . 7 ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V)
232187, 2, 231mp2an 704 . . . . . 6 𝐺 ∈ V
233 feq1 5939 . . . . . . 7 (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴𝐺:(cf‘𝐴)⟶𝐴))
234 smoeq 7334 . . . . . . 7 (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺))
235 fveq1 6102 . . . . . . . . . 10 (𝑓 = 𝐺 → (𝑓𝑤) = (𝐺𝑤))
236235sseq2d 3596 . . . . . . . . 9 (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓𝑤) ↔ 𝑧 ⊆ (𝐺𝑤)))
237236rexbidv 3034 . . . . . . . 8 (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)))
238237ralbidv 2969 . . . . . . 7 (𝑓 = 𝐺 → (∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤) ↔ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)))
239233, 234, 2383anbi123d 1391 . . . . . 6 (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤))))
240232, 239spcev 3273 . . . . 5 ((𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
241191, 218, 230, 240syl3anc 1318 . . . 4 (((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) ∧ 𝐴 ∈ On) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
242241expcom 450 . . 3 (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤))))
243242exlimdv 1848 . 2 (𝐴 ∈ On → (∃𝑔(𝑔:(cf‘𝐴)–1-1𝐴 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤))))
2441, 243mpd 15 1 (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧𝐴𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓𝑤)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383  w3a 1031   = wceq 1475  wex 1695  wcel 1977  wral 2896  wrex 2897  Vcvv 3173  cun 3538  wss 3540   ciun 4455  cmpt 4643  dom cdm 5038  cres 5040  Ord word 5639  Oncon0 5640  suc csuc 5642  Fun wfun 5798   Fn wfn 5799  wf 5800  1-1wf1 5801  cfv 5804  Smo wsmo 7329  recscrecs 7354  cfccf 8646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-smo 7330  df-recs 7355  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-card 8648  df-cf 8650  df-acn 8651
This theorem is referenced by:  cfsmo  8976
  Copyright terms: Public domain W3C validator