ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  hashunlem GIF version

Theorem hashunlem 10109
Description: Lemma for hashun 10110. Ordinal size of the union. (Contributed by Jim Kingdon, 25-Feb-2022.)
Hypotheses
Ref Expression
hashunlem.a (𝜑𝐴 ∈ Fin)
hashunlem.b (𝜑𝐵 ∈ Fin)
hashunlem.disj (𝜑 → (𝐴𝐵) = ∅)
hashunlem.n (𝜑𝑁 ∈ ω)
hashunlem.m (𝜑𝑀 ∈ ω)
hashunlem.an (𝜑𝐴𝑁)
hashunlem.bm (𝜑𝐵𝑀)
Assertion
Ref Expression
hashunlem (𝜑 → (𝐴𝐵) ≈ (𝑁 +𝑜 𝑀))

Proof of Theorem hashunlem
Dummy variables 𝑗 𝑤 𝑘 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 3823 . . . . 5 (𝑤 = ∅ → (𝑤𝑗 ↔ ∅ ≈ 𝑗))
2 uneq2 3137 . . . . . 6 (𝑤 = ∅ → (𝐴𝑤) = (𝐴 ∪ ∅))
32breq1d 3830 . . . . 5 (𝑤 = ∅ → ((𝐴𝑤) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗)))
41, 3anbi12d 457 . . . 4 (𝑤 = ∅ → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗))))
54rexbidv 2377 . . 3 (𝑤 = ∅ → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗))))
6 breq1 3823 . . . . 5 (𝑤 = 𝑦 → (𝑤𝑗𝑦𝑗))
7 uneq2 3137 . . . . . 6 (𝑤 = 𝑦 → (𝐴𝑤) = (𝐴𝑦))
87breq1d 3830 . . . . 5 (𝑤 = 𝑦 → ((𝐴𝑤) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗)))
96, 8anbi12d 457 . . . 4 (𝑤 = 𝑦 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))))
109rexbidv 2377 . . 3 (𝑤 = 𝑦 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))))
11 breq1 3823 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑗))
12 uneq2 3137 . . . . . 6 (𝑤 = (𝑦 ∪ {𝑧}) → (𝐴𝑤) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
1312breq1d 3830 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐴𝑤) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗)))
1411, 13anbi12d 457 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗))))
1514rexbidv 2377 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗))))
16 breq1 3823 . . . . 5 (𝑤 = 𝐵 → (𝑤𝑗𝐵𝑗))
17 uneq2 3137 . . . . . 6 (𝑤 = 𝐵 → (𝐴𝑤) = (𝐴𝐵))
1817breq1d 3830 . . . . 5 (𝑤 = 𝐵 → ((𝐴𝑤) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))
1916, 18anbi12d 457 . . . 4 (𝑤 = 𝐵 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗))))
2019rexbidv 2377 . . 3 (𝑤 = 𝐵 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗))))
21 peano1 4382 . . . . 5 ∅ ∈ ω
2221a1i 9 . . . 4 (𝜑 → ∅ ∈ ω)
23 0ex 3941 . . . . . 6 ∅ ∈ V
2423enref 6434 . . . . 5 ∅ ≈ ∅
2524a1i 9 . . . 4 (𝜑 → ∅ ≈ ∅)
26 hashunlem.an . . . . 5 (𝜑𝐴𝑁)
27 un0 3305 . . . . . 6 (𝐴 ∪ ∅) = 𝐴
2827a1i 9 . . . . 5 (𝜑 → (𝐴 ∪ ∅) = 𝐴)
29 hashunlem.n . . . . . 6 (𝜑𝑁 ∈ ω)
30 nna0 6189 . . . . . 6 (𝑁 ∈ ω → (𝑁 +𝑜 ∅) = 𝑁)
3129, 30syl 14 . . . . 5 (𝜑 → (𝑁 +𝑜 ∅) = 𝑁)
3226, 28, 313brtr4d 3850 . . . 4 (𝜑 → (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 ∅))
33 breq2 3824 . . . . . 6 (𝑗 = ∅ → (∅ ≈ 𝑗 ↔ ∅ ≈ ∅))
34 oveq2 5621 . . . . . . 7 (𝑗 = ∅ → (𝑁 +𝑜 𝑗) = (𝑁 +𝑜 ∅))
3534breq2d 3832 . . . . . 6 (𝑗 = ∅ → ((𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 ∅)))
3633, 35anbi12d 457 . . . . 5 (𝑗 = ∅ → ((∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗)) ↔ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 ∅))))
3736rspcev 2715 . . . 4 ((∅ ∈ ω ∧ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 ∅))) → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗)))
3822, 25, 32, 37syl12anc 1170 . . 3 (𝜑 → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗)))
39 peano2 4383 . . . . . . . 8 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
4039ad2antlr 473 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → suc 𝑗 ∈ ω)
41 simp-4r 509 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑦 ∈ Fin)
42 vex 2618 . . . . . . . . . 10 𝑧 ∈ V
4342a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧 ∈ V)
44 simprr 499 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → 𝑧 ∈ (𝐵𝑦))
4544ad2antrr 472 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧 ∈ (𝐵𝑦))
4645eldifbd 3000 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ¬ 𝑧𝑦)
4743, 46eldifd 2998 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧 ∈ (V ∖ 𝑦))
48 simplr 497 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑗 ∈ ω)
49 simprl 498 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑦𝑗)
50 fiunsnnn 6549 . . . . . . . 8 (((𝑦 ∈ Fin ∧ 𝑧 ∈ (V ∖ 𝑦)) ∧ (𝑗 ∈ ω ∧ 𝑦𝑗)) → (𝑦 ∪ {𝑧}) ≈ suc 𝑗)
5141, 47, 48, 49, 50syl22anc 1173 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝑦 ∪ {𝑧}) ≈ suc 𝑗)
52 hashunlem.a . . . . . . . . . . 11 (𝜑𝐴 ∈ Fin)
5352ad4antr 478 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝐴 ∈ Fin)
54 simprl 498 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → 𝑦𝐵)
5554ad2antrr 472 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑦𝐵)
56 hashunlem.disj . . . . . . . . . . . 12 (𝜑 → (𝐴𝐵) = ∅)
5756ad4antr 478 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴𝐵) = ∅)
58 incom 3181 . . . . . . . . . . . 12 (𝑦𝐴) = (𝐴𝑦)
59 incom 3181 . . . . . . . . . . . . . 14 (𝐴𝐵) = (𝐵𝐴)
6059eqeq1i 2092 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
61 ssdisj 3327 . . . . . . . . . . . . 13 ((𝑦𝐵 ∧ (𝐵𝐴) = ∅) → (𝑦𝐴) = ∅)
6260, 61sylan2b 281 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝑦𝐴) = ∅)
6358, 62syl5eqr 2131 . . . . . . . . . . 11 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝐴𝑦) = ∅)
6455, 57, 63syl2anc 403 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴𝑦) = ∅)
65 unfidisj 6584 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ∧ (𝐴𝑦) = ∅) → (𝐴𝑦) ∈ Fin)
6653, 41, 64, 65syl3anc 1172 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴𝑦) ∈ Fin)
6745eldifad 2999 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧𝐵)
68 minel 3332 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (𝐴𝐵) = ∅) → ¬ 𝑧𝐴)
6967, 57, 68syl2anc 403 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ¬ 𝑧𝐴)
70 ioran 702 . . . . . . . . . . . 12 (¬ (𝑧𝐴𝑧𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
71 elun 3130 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
7270, 71xchnxbir 639 . . . . . . . . . . 11 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
7369, 46, 72sylanbrc 408 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ¬ 𝑧 ∈ (𝐴𝑦))
7443, 73eldifd 2998 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧 ∈ (V ∖ (𝐴𝑦)))
7529ad4antr 478 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑁 ∈ ω)
76 nnacl 6195 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +𝑜 𝑗) ∈ ω)
7775, 48, 76syl2anc 403 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝑁 +𝑜 𝑗) ∈ ω)
78 simprr 499 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))
79 fiunsnnn 6549 . . . . . . . . 9 ((((𝐴𝑦) ∈ Fin ∧ 𝑧 ∈ (V ∖ (𝐴𝑦))) ∧ ((𝑁 +𝑜 𝑗) ∈ ω ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +𝑜 𝑗))
8066, 74, 77, 78, 79syl22anc 1173 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +𝑜 𝑗))
81 unass 3146 . . . . . . . . . 10 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
8281a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
8382eqcomd 2090 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ {𝑧}))
84 nnasuc 6191 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +𝑜 suc 𝑗) = suc (𝑁 +𝑜 𝑗))
8575, 48, 84syl2anc 403 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝑁 +𝑜 suc 𝑗) = suc (𝑁 +𝑜 𝑗))
8680, 83, 853brtr4d 3850 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 suc 𝑗))
87 breq2 3824 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝑦 ∪ {𝑧}) ≈ 𝑘 ↔ (𝑦 ∪ {𝑧}) ≈ suc 𝑗))
88 oveq2 5621 . . . . . . . . . 10 (𝑘 = suc 𝑗 → (𝑁 +𝑜 𝑘) = (𝑁 +𝑜 suc 𝑗))
8988breq2d 3832 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 suc 𝑗)))
9087, 89anbi12d 457 . . . . . . . 8 (𝑘 = suc 𝑗 → (((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)) ↔ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 suc 𝑗))))
9190rspcev 2715 . . . . . . 7 ((suc 𝑗 ∈ ω ∧ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 suc 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)))
9240, 51, 86, 91syl12anc 1170 . . . . . 6 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)))
9392ex 113 . . . . 5 ((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) → ((𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘))))
9493rexlimdva 2485 . . . 4 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘))))
95 breq2 3824 . . . . . 6 (𝑗 = 𝑘 → ((𝑦 ∪ {𝑧}) ≈ 𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑘))
96 oveq2 5621 . . . . . . 7 (𝑗 = 𝑘 → (𝑁 +𝑜 𝑗) = (𝑁 +𝑜 𝑘))
9796breq2d 3832 . . . . . 6 (𝑗 = 𝑘 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)))
9895, 97anbi12d 457 . . . . 5 (𝑗 = 𝑘 → (((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘))))
9998cbvrexv 2587 . . . 4 (∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)))
10094, 99syl6ibr 160 . . 3 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗)) → ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗))))
101 hashunlem.b . . 3 (𝜑𝐵 ∈ Fin)
1025, 10, 15, 20, 38, 100, 101findcard2sd 6560 . 2 (𝜑 → ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))
103 simprrr 507 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗))
104 hashunlem.bm . . . . . . 7 (𝜑𝐵𝑀)
105104ensymd 6452 . . . . . 6 (𝜑𝑀𝐵)
106 simprrl 506 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → 𝐵𝑗)
107 entr 6453 . . . . . 6 ((𝑀𝐵𝐵𝑗) → 𝑀𝑗)
108105, 106, 107syl2an2r 560 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → 𝑀𝑗)
109 hashunlem.m . . . . . 6 (𝜑𝑀 ∈ ω)
110 simprl 498 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → 𝑗 ∈ ω)
111 nneneq 6525 . . . . . 6 ((𝑀 ∈ ω ∧ 𝑗 ∈ ω) → (𝑀𝑗𝑀 = 𝑗))
112109, 110, 111syl2an2r 560 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → (𝑀𝑗𝑀 = 𝑗))
113108, 112mpbid 145 . . . 4 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → 𝑀 = 𝑗)
114113oveq2d 5629 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → (𝑁 +𝑜 𝑀) = (𝑁 +𝑜 𝑗))
115103, 114breqtrrd 3846 . 2 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +𝑜 𝑀))
116102, 115rexlimddv 2489 1 (𝜑 → (𝐴𝐵) ≈ (𝑁 +𝑜 𝑀))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662   = wceq 1287  wcel 1436  wrex 2356  Vcvv 2615  cdif 2985  cun 2986  cin 2987  wss 2988  c0 3275  {csn 3431   class class class wbr 3820  suc csuc 4166  ωcom 4378  (class class class)co 5613   +𝑜 coa 6132  cen 6407  Fincfn 6409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3929  ax-sep 3932  ax-nul 3940  ax-pow 3984  ax-pr 4010  ax-un 4234  ax-setind 4326  ax-iinf 4376
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-if 3380  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-int 3672  df-iun 3715  df-br 3821  df-opab 3875  df-mpt 3876  df-tr 3912  df-id 4094  df-iord 4167  df-on 4169  df-suc 4172  df-iom 4379  df-xp 4417  df-rel 4418  df-cnv 4419  df-co 4420  df-dm 4421  df-rn 4422  df-res 4423  df-ima 4424  df-iota 4946  df-fun 4983  df-fn 4984  df-f 4985  df-f1 4986  df-fo 4987  df-f1o 4988  df-fv 4989  df-ov 5616  df-oprab 5617  df-mpt2 5618  df-1st 5868  df-2nd 5869  df-recs 6024  df-irdg 6089  df-1o 6135  df-oadd 6139  df-er 6244  df-en 6410  df-fin 6412
This theorem is referenced by:  hashun  10110
  Copyright terms: Public domain W3C validator