Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cantnfresb Structured version   Visualization version   GIF version

Theorem cantnfresb 43313
Description: A Cantor normal form which sums to less than a certain power has only zeros for larger components. (Contributed by RP, 3-Feb-2025.)
Assertion
Ref Expression
cantnfresb (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶) ↔ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐹

Proof of Theorem cantnfresb
Dummy variables 𝑎 𝑏 𝑐 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2734 . . . . . . . . . . 11 dom (𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵)
2 eldifi 4140 . . . . . . . . . . . 12 (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
32adantr 480 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → 𝐴 ∈ On)
4 simpr 484 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
5 eqid 2734 . . . . . . . . . . 11 {⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))}
61, 3, 4, 5cantnf 9730 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴o 𝐵)))
76adantr 480 . . . . . . . . 9 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴o 𝐵)))
8 simpr 484 . . . . . . . . 9 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
9 ondif2 8538 . . . . . . . . . . . . . . 15 (𝐴 ∈ (On ∖ 2o) ↔ (𝐴 ∈ On ∧ 1o𝐴))
109simprbi 496 . . . . . . . . . . . . . 14 (𝐴 ∈ (On ∖ 2o) → 1o𝐴)
11 dif20el 8541 . . . . . . . . . . . . . 14 (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
1210, 11ifcld 4576 . . . . . . . . . . . . 13 (𝐴 ∈ (On ∖ 2o) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴)
1312ad2antrr 726 . . . . . . . . . . . 12 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝑦𝐵) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴)
1413fmpttd 7134 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵𝐴)
1511adantr 480 . . . . . . . . . . . 12 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ∅ ∈ 𝐴)
16 eqid 2734 . . . . . . . . . . . 12 (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))
174, 15, 16sniffsupp 9437 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp ∅)
181, 3, 4cantnfs 9703 . . . . . . . . . . 11 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵𝐴 ∧ (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp ∅)))
1914, 17, 18mpbir2and 713 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))
2019adantr 480 . . . . . . . . 9 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))
21 isorel 7345 . . . . . . . . 9 (((𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴o 𝐵)) ∧ (𝐹 ∈ dom (𝐴 CNF 𝐵) ∧ (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
227, 8, 20, 21syl12anc 837 . . . . . . . 8 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
2322adantrl 716 . . . . . . 7 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
2423adantr 480 . . . . . 6 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
25 fvexd 6921 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶𝐵) → ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈ V)
26 epelg 5589 . . . . . . 7 (((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈ V → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
2725, 26syl 17 . . . . . 6 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶𝐵) → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
282ad2antrr 726 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶𝐵) → 𝐴 ∈ On)
29 simplr 769 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶𝐵) → 𝐵 ∈ On)
30 fconst6g 6797 . . . . . . . . . . . . . . . . . 18 (∅ ∈ 𝐴 → (𝐵 × {∅}):𝐵𝐴)
3111, 30syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ (On ∖ 2o) → (𝐵 × {∅}):𝐵𝐴)
3231adantr 480 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}):𝐵𝐴)
334, 15fczfsuppd 9423 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) finSupp ∅)
341, 3, 4cantnfs 9703 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
3532, 33, 34mpbir2and 713 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
3635adantr 480 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶𝐵) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
37 simpr 484 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶𝐵) → 𝐶𝐵)
3810ad2antrr 726 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶𝐵) → 1o𝐴)
39 fczsupp0 8216 . . . . . . . . . . . . . . . 16 ((𝐵 × {∅}) supp ∅) = ∅
40 0ss 4405 . . . . . . . . . . . . . . . 16 ∅ ⊆ 𝐶
4139, 40eqsstri 4029 . . . . . . . . . . . . . . 15 ((𝐵 × {∅}) supp ∅) ⊆ 𝐶
4241a1i 11 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶𝐵) → ((𝐵 × {∅}) supp ∅) ⊆ 𝐶)
43 0ex 5312 . . . . . . . . . . . . . . . . . 18 ∅ ∈ V
4443fvconst2 7223 . . . . . . . . . . . . . . . . 17 (𝑦𝐵 → ((𝐵 × {∅})‘𝑦) = ∅)
4544ifeq2d 4550 . . . . . . . . . . . . . . . 16 (𝑦𝐵 → if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)) = if(𝑦 = 𝐶, 1o, ∅))
4645mpteq2ia 5250 . . . . . . . . . . . . . . 15 (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦))) = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))
4746eqcomi 2743 . . . . . . . . . . . . . 14 (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)))
481, 28, 29, 36, 37, 38, 42, 47cantnfp1 9718 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶𝐵) → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ∧ ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))))
4948simprd 495 . . . . . . . . . . . 12 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶𝐵) → ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
5049adantrl 716 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
51 oecl 8573 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴o 𝐶) ∈ On)
523, 51sylan 580 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴o 𝐶) ∈ On)
53 om1 8578 . . . . . . . . . . . . . . 15 ((𝐴o 𝐶) ∈ On → ((𝐴o 𝐶) ·o 1o) = (𝐴o 𝐶))
5452, 53syl 17 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴o 𝐶) ·o 1o) = (𝐴o 𝐶))
551, 3, 4, 15cantnf0 9712 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
5655adantr 480 . . . . . . . . . . . . . 14 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
5754, 56oveq12d 7448 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = ((𝐴o 𝐶) +o ∅))
58 oa0 8552 . . . . . . . . . . . . . 14 ((𝐴o 𝐶) ∈ On → ((𝐴o 𝐶) +o ∅) = (𝐴o 𝐶))
5952, 58syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴o 𝐶) +o ∅) = (𝐴o 𝐶))
6057, 59eqtrd 2774 . . . . . . . . . . . 12 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴o 𝐶))
6160adantrr 717 . . . . . . . . . . 11 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶𝐵)) → (((𝐴o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴o 𝐶))
6250, 61eqtrd 2774 . . . . . . . . . 10 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (𝐴o 𝐶))
6362eleq2d 2824 . . . . . . . . 9 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶𝐵)) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶)))
6463exp32 420 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐶 ∈ On → (𝐶𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶)))))
6564adantrd 491 . . . . . . 7 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐶𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶)))))
6665imp31 417 . . . . . 6 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶)))
6724, 27, 663bitrrd 306 . . . . 5 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶) ↔ 𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))))
68 fveq1 6905 . . . . . . . . . . 11 (𝑎 = 𝐹 → (𝑎𝑐) = (𝐹𝑐))
6968eleq1d 2823 . . . . . . . . . 10 (𝑎 = 𝐹 → ((𝑎𝑐) ∈ (𝑏𝑐) ↔ (𝐹𝑐) ∈ (𝑏𝑐)))
70 fveq1 6905 . . . . . . . . . . . . 13 (𝑎 = 𝐹 → (𝑎𝑥) = (𝐹𝑥))
7170eqeq1d 2736 . . . . . . . . . . . 12 (𝑎 = 𝐹 → ((𝑎𝑥) = (𝑏𝑥) ↔ (𝐹𝑥) = (𝑏𝑥)))
7271imbi2d 340 . . . . . . . . . . 11 (𝑎 = 𝐹 → ((𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)) ↔ (𝑐𝑥 → (𝐹𝑥) = (𝑏𝑥))))
7372ralbidv 3175 . . . . . . . . . 10 (𝑎 = 𝐹 → (∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)) ↔ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = (𝑏𝑥))))
7469, 73anbi12d 632 . . . . . . . . 9 (𝑎 = 𝐹 → (((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥))) ↔ ((𝐹𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = (𝑏𝑥)))))
7574rexbidv 3176 . . . . . . . 8 (𝑎 = 𝐹 → (∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥))) ↔ ∃𝑐𝐵 ((𝐹𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = (𝑏𝑥)))))
76 fveq1 6905 . . . . . . . . . . 11 (𝑏 = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏𝑐) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐))
7776eleq2d 2824 . . . . . . . . . 10 (𝑏 = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹𝑐) ∈ (𝑏𝑐) ↔ (𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)))
78 fveq1 6905 . . . . . . . . . . . . 13 (𝑏 = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))
7978eqeq2d 2745 . . . . . . . . . . . 12 (𝑏 = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹𝑥) = (𝑏𝑥) ↔ (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))
8079imbi2d 340 . . . . . . . . . . 11 (𝑏 = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝑐𝑥 → (𝐹𝑥) = (𝑏𝑥)) ↔ (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
8180ralbidv 3175 . . . . . . . . . 10 (𝑏 = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = (𝑏𝑥)) ↔ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
8277, 81anbi12d 632 . . . . . . . . 9 (𝑏 = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (((𝐹𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = (𝑏𝑥))) ↔ ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
8382rexbidv 3176 . . . . . . . 8 (𝑏 = (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (∃𝑐𝐵 ((𝐹𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = (𝑏𝑥))) ↔ ∃𝑐𝐵 ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
8475, 83, 5bropabg 43312 . . . . . . 7 (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐹 ∈ V ∧ (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧ ∃𝑐𝐵 ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
85 fveq2 6906 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝐶 → (𝐹𝑐) = (𝐹𝐶))
8685adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑐 = 𝐶𝑐𝐵) → (𝐹𝑐) = (𝐹𝐶))
87 eqeq1 2738 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑐 → (𝑦 = 𝐶𝑐 = 𝐶))
8887ifbid 4553 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑐 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑐 = 𝐶, 1o, ∅))
89 1oex 8514 . . . . . . . . . . . . . . . . . . . 20 1o ∈ V
9089, 43ifex 4580 . . . . . . . . . . . . . . . . . . 19 if(𝑐 = 𝐶, 1o, ∅) ∈ V
9188, 16, 90fvmpt 7015 . . . . . . . . . . . . . . . . . 18 (𝑐𝐵 → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅))
92 iftrue 4536 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝐶 → if(𝑐 = 𝐶, 1o, ∅) = 1o)
9391, 92sylan9eqr 2796 . . . . . . . . . . . . . . . . 17 ((𝑐 = 𝐶𝑐𝐵) → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = 1o)
9486, 93eleq12d 2832 . . . . . . . . . . . . . . . 16 ((𝑐 = 𝐶𝑐𝐵) → ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹𝐶) ∈ 1o))
95 el1o 8531 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐶) ∈ 1o ↔ (𝐹𝐶) = ∅)
9695a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑐 = 𝐶𝑐𝐵) → ((𝐹𝐶) ∈ 1o ↔ (𝐹𝐶) = ∅))
9796biimpd 229 . . . . . . . . . . . . . . . . 17 ((𝑐 = 𝐶𝑐𝐵) → ((𝐹𝐶) ∈ 1o → (𝐹𝐶) = ∅))
98 simpl 482 . . . . . . . . . . . . . . . . 17 ((𝑐 = 𝐶𝑐𝐵) → 𝑐 = 𝐶)
9997, 98jctild 525 . . . . . . . . . . . . . . . 16 ((𝑐 = 𝐶𝑐𝐵) → ((𝐹𝐶) ∈ 1o → (𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅)))
10094, 99sylbid 240 . . . . . . . . . . . . . . 15 ((𝑐 = 𝐶𝑐𝐵) → ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅)))
101100expimpd 453 . . . . . . . . . . . . . 14 (𝑐 = 𝐶 → ((𝑐𝐵 ∧ (𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅)))
10291adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝐶𝑐𝐵) → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅))
103 simpl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐𝐶𝑐𝐵) → 𝑐𝐶)
104103neneqd 2942 . . . . . . . . . . . . . . . . . . . 20 ((𝑐𝐶𝑐𝐵) → ¬ 𝑐 = 𝐶)
105104iffalsed 4541 . . . . . . . . . . . . . . . . . . 19 ((𝑐𝐶𝑐𝐵) → if(𝑐 = 𝐶, 1o, ∅) = ∅)
106102, 105eqtrd 2774 . . . . . . . . . . . . . . . . . 18 ((𝑐𝐶𝑐𝐵) → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = ∅)
107106eleq2d 2824 . . . . . . . . . . . . . . . . 17 ((𝑐𝐶𝑐𝐵) → ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹𝑐) ∈ ∅))
108107biimpd 229 . . . . . . . . . . . . . . . 16 ((𝑐𝐶𝑐𝐵) → ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝐹𝑐) ∈ ∅))
109108expimpd 453 . . . . . . . . . . . . . . 15 (𝑐𝐶 → ((𝑐𝐵 ∧ (𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝐹𝑐) ∈ ∅))
110 noel 4343 . . . . . . . . . . . . . . . 16 ¬ (𝐹𝑐) ∈ ∅
111110pm2.21i 119 . . . . . . . . . . . . . . 15 ((𝐹𝑐) ∈ ∅ → (𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅))
112109, 111syl6 35 . . . . . . . . . . . . . 14 (𝑐𝐶 → ((𝑐𝐵 ∧ (𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅)))
113101, 112pm2.61ine 3022 . . . . . . . . . . . . 13 ((𝑐𝐵 ∧ (𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅))
114113a1i 11 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → ((𝑐𝐵 ∧ (𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅)))
115 fveqeq2 6915 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐶 → ((𝐹𝑥) = ∅ ↔ (𝐹𝐶) = ∅))
116115ralsng 4679 . . . . . . . . . . . . . . 15 (𝐶𝐵 → (∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅ ↔ (𝐹𝐶) = ∅))
117116anbi2d 630 . . . . . . . . . . . . . 14 (𝐶𝐵 → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅) ↔ (𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅)))
118117biimprd 248 . . . . . . . . . . . . 13 (𝐶𝐵 → ((𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅)))
119118adantl 481 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → ((𝑐 = 𝐶 ∧ (𝐹𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅)))
1204anim1i 615 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
121120adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
122 pm3.31 449 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝐵 → (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥𝐵𝑐𝑥) → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))
123122a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥𝐵 → (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥𝐵𝑐𝑥) → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
124 eldif 3972 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶))
125 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → 𝑐 = 𝐶)
126125eleq1d 2823 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → (𝑐𝑥𝐶𝑥))
127 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
128127adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐵 ∈ On)
129 onelon 6410 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐵 ∈ On ∧ 𝑥𝐵) → 𝑥 ∈ On)
130128, 129sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → 𝑥 ∈ On)
131 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → 𝐶 ∈ On)
132 ontri1 6419 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥𝐶 ↔ ¬ 𝐶𝑥))
133130, 131, 132syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → (𝑥𝐶 ↔ ¬ 𝐶𝑥))
134133con2bid 354 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → (𝐶𝑥 ↔ ¬ 𝑥𝐶))
135 onsssuc 6475 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥𝐶𝑥 ∈ suc 𝐶))
136130, 131, 135syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → (𝑥𝐶𝑥 ∈ suc 𝐶))
137136notbid 318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → (¬ 𝑥𝐶 ↔ ¬ 𝑥 ∈ suc 𝐶))
138126, 134, 1373bitrrd 306 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥𝐵) → (¬ 𝑥 ∈ suc 𝐶𝑐𝑥))
139138pm5.32da 579 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶) ↔ (𝑥𝐵𝑐𝑥)))
140124, 139bitrid 283 . . . . . . . . . . . . . . . . . . . 20 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥𝐵𝑐𝑥)))
141140biimpd 229 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝑥𝐵𝑐𝑥)))
142141imim1d 82 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (((𝑥𝐵𝑐𝑥) → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
143 eldifi 4140 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (𝐵 ∖ suc 𝐶) → 𝑥𝐵)
144143adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥𝐵)
145 eqeq1 2738 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (𝑦 = 𝐶𝑥 = 𝐶))
146145ifbid 4553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑥 = 𝐶, 1o, ∅))
14789, 43ifex 4580 . . . . . . . . . . . . . . . . . . . . . . . . 25 if(𝑥 = 𝐶, 1o, ∅) ∈ V
148146, 16, 147fvmpt 7015 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐵 → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅))
149144, 148syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅))
150128, 143, 129syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ On)
151 eloni 6395 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ On → Ord 𝑥)
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → Ord 𝑥)
153 eloni 6395 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐵 ∈ On → Ord 𝐵)
154153ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → Ord 𝐵)
155 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐶 ∈ On)
156 ordeldifsucon 43248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Ord 𝐵𝐶 ∈ On) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥𝐵𝐶𝑥)))
157154, 155, 156syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥𝐵𝐶𝑥)))
158157biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → (𝑥𝐵𝐶𝑥))
159 ordirr 6403 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Ord 𝑥 → ¬ 𝑥𝑥)
160 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝐶 → (𝑥𝑥𝐶𝑥))
161160notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝐶 → (¬ 𝑥𝑥 ↔ ¬ 𝐶𝑥))
162159, 161syl5ibcom 245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Ord 𝑥 → (𝑥 = 𝐶 → ¬ 𝐶𝑥))
163162con2d 134 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord 𝑥 → (𝐶𝑥 → ¬ 𝑥 = 𝐶))
164163adantld 490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝑥 → ((𝑥𝐵𝐶𝑥) → ¬ 𝑥 = 𝐶))
165152, 158, 164sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ¬ 𝑥 = 𝐶)
166165iffalsed 4541 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → if(𝑥 = 𝐶, 1o, ∅) = ∅)
167149, 166eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = ∅)
168167eqeq2d 2745 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) ↔ (𝐹𝑥) = ∅))
169168biimpd 229 . . . . . . . . . . . . . . . . . . . 20 ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹𝑥) = ∅))
170169ex 412 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → ((𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹𝑥) = ∅)))
171170a2d 29 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹𝑥) = ∅)))
172123, 142, 1713syld 60 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥𝐵 → (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹𝑥) = ∅)))
173172ralimdv2 3160 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹𝑥) = ∅))
174121, 173sylan 580 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹𝑥) = ∅))
175174adantr 480 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅) → (∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹𝑥) = ∅))
176 ralun 4207 . . . . . . . . . . . . . . . . 17 ((∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅ ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹𝑥) = ∅)
177176adantll 714 . . . . . . . . . . . . . . . 16 (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹𝑥) = ∅)
178 undif3 4305 . . . . . . . . . . . . . . . . . . . . 21 ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶}))
179 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐶 ∈ On ∧ 𝐶𝐵) → 𝐶𝐵)
180179snssd 4813 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ∈ On ∧ 𝐶𝐵) → {𝐶} ⊆ 𝐵)
181 ssequn1 4195 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∪ 𝐵) = 𝐵)
182180, 181sylib 218 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ On ∧ 𝐶𝐵) → ({𝐶} ∪ 𝐵) = 𝐵)
183 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐶 ∈ On ∧ 𝐶𝐵) → 𝐶 ∈ On)
184 eloni 6395 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐶 ∈ On → Ord 𝐶)
185 orddif 6481 . . . . . . . . . . . . . . . . . . . . . . . 24 (Ord 𝐶𝐶 = (suc 𝐶 ∖ {𝐶}))
186183, 184, 1853syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ∈ On ∧ 𝐶𝐵) → 𝐶 = (suc 𝐶 ∖ {𝐶}))
187186eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐶 ∈ On ∧ 𝐶𝐵) → (suc 𝐶 ∖ {𝐶}) = 𝐶)
188182, 187difeq12d 4136 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ On ∧ 𝐶𝐵) → (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) = (𝐵𝐶))
189178, 188eqtrid 2786 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 ∈ On ∧ 𝐶𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵𝐶))
190189adantll 714 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵𝐶))
191190adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵𝐶))
192191raleqdv 3323 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
193192ad2antrr 726 . . . . . . . . . . . . . . . 16 (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹𝑥) = ∅) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
194177, 193mpbid 232 . . . . . . . . . . . . . . 15 (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹𝑥) = ∅) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅)
195194ex 412 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅) → (∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹𝑥) = ∅ → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
196175, 195syld 47 . . . . . . . . . . . . 13 ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅) → (∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
197196expl 457 . . . . . . . . . . . 12 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹𝑥) = ∅) → (∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅)))
198114, 119, 1973syld 60 . . . . . . . . . . 11 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → ((𝑐𝐵 ∧ (𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅)))
199198expdimp 452 . . . . . . . . . 10 (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐𝐵) → ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅)))
200199impd 410 . . . . . . . . 9 (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) ∧ 𝑐𝐵) → (((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
201200rexlimdva 3152 . . . . . . . 8 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → (∃𝑐𝐵 ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
202201adantld 490 . . . . . . 7 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → (((𝐹 ∈ V ∧ (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧ ∃𝑐𝐵 ((𝐹𝑐) ∈ ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝐹𝑥) = ((𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
20384, 202biimtrid 242 . . . . . 6 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
204203adantlrr 721 . . . . 5 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐𝐵 ((𝑎𝑐) ∈ (𝑏𝑐) ∧ ∀𝑥𝐵 (𝑐𝑥 → (𝑎𝑥) = (𝑏𝑥)))} (𝑦𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
20567, 204sylbid 240 . . . 4 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
206205ex 412 . . 3 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅)))
207 ral0 4518 . . . . 5 𝑥 ∈ ∅ (𝐹𝑥) = ∅
208 ssdif0 4371 . . . . . . 7 (𝐵𝐶 ↔ (𝐵𝐶) = ∅)
209208biimpi 216 . . . . . 6 (𝐵𝐶 → (𝐵𝐶) = ∅)
210209raleqdv 3323 . . . . 5 (𝐵𝐶 → (∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅ ↔ ∀𝑥 ∈ ∅ (𝐹𝑥) = ∅))
211207, 210mpbiri 258 . . . 4 (𝐵𝐶 → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅)
212211a1i13 27 . . 3 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐵𝐶 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅)))
213184adantr 480 . . . 4 ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → Ord 𝐶)
214153adantl 481 . . . 4 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → Ord 𝐵)
215 ordtri2or 6483 . . . 4 ((Ord 𝐶 ∧ Ord 𝐵) → (𝐶𝐵𝐵𝐶))
216213, 214, 215syl2anr 597 . . 3 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶𝐵𝐵𝐶))
217206, 212, 216mpjaod 860 . 2 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶) → ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
2183ad2antrr 726 . . . 4 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → 𝐴 ∈ On)
219 simpllr 776 . . . 4 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → 𝐵 ∈ On)
220 simplrr 778 . . . 4 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
22115ad2antrr 726 . . . 4 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → ∅ ∈ 𝐴)
222 simplrl 777 . . . 4 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → 𝐶 ∈ On)
2231, 3, 4cantnfs 9703 . . . . . . . . . 10 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
224223biimpd 229 . . . . . . . . 9 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) → (𝐹:𝐵𝐴𝐹 finSupp ∅)))
225224adantld 490 . . . . . . . 8 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹:𝐵𝐴𝐹 finSupp ∅)))
226225imp 406 . . . . . . 7 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹:𝐵𝐴𝐹 finSupp ∅))
227226simpld 494 . . . . . 6 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → 𝐹:𝐵𝐴)
228227adantr 480 . . . . 5 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → 𝐹:𝐵𝐴)
229 fveqeq2 6915 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐹𝑥) = ∅ ↔ (𝐹𝑦) = ∅))
230229rspccv 3618 . . . . . . 7 (∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅ → (𝑦 ∈ (𝐵𝐶) → (𝐹𝑦) = ∅))
231230adantl 481 . . . . . 6 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → (𝑦 ∈ (𝐵𝐶) → (𝐹𝑦) = ∅))
232231imp 406 . . . . 5 (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) ∧ 𝑦 ∈ (𝐵𝐶)) → (𝐹𝑦) = ∅)
233228, 232suppss 8217 . . . 4 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → (𝐹 supp ∅) ⊆ 𝐶)
2341, 218, 219, 220, 221, 222, 233cantnflt2 9710 . . 3 ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅) → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶))
235234ex 412 . 2 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅ → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶)))
236217, 235impbid 212 1 (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴o 𝐶) ↔ ∀𝑥 ∈ (𝐵𝐶)(𝐹𝑥) = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cdif 3959  cun 3960  wss 3962  c0 4338  ifcif 4530  {csn 4630   class class class wbr 5147  {copab 5209  cmpt 5230   E cep 5587   × cxp 5686  dom cdm 5688  Ord word 6384  Oncon0 6385  suc csuc 6387  wf 6558  cfv 6562   Isom wiso 6563  (class class class)co 7430   supp csupp 8183  1oc1o 8497  2oc2o 8498   +o coa 8501   ·o comu 8502  o coe 8503   finSupp cfsupp 9398   CNF ccnf 9698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-seqom 8486  df-1o 8504  df-2o 8505  df-oadd 8508  df-omul 8509  df-oexp 8510  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-oi 9547  df-cnf 9699
This theorem is referenced by:  cantnf2  43314
  Copyright terms: Public domain W3C validator