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

Theorem hashunlem 10047
Description: Lemma for hashun 10048. 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 3814 . . . . 5 (𝑤 = ∅ → (𝑤𝑗 ↔ ∅ ≈ 𝑗))
2 uneq2 3132 . . . . . 6 (𝑤 = ∅ → (𝐴𝑤) = (𝐴 ∪ ∅))
32breq1d 3821 . . . . 5 (𝑤 = ∅ → ((𝐴𝑤) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗)))
41, 3anbi12d 457 . . . 4 (𝑤 = ∅ → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗))))
54rexbidv 2375 . . 3 (𝑤 = ∅ → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗))))
6 breq1 3814 . . . . 5 (𝑤 = 𝑦 → (𝑤𝑗𝑦𝑗))
7 uneq2 3132 . . . . . 6 (𝑤 = 𝑦 → (𝐴𝑤) = (𝐴𝑦))
87breq1d 3821 . . . . 5 (𝑤 = 𝑦 → ((𝐴𝑤) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗)))
96, 8anbi12d 457 . . . 4 (𝑤 = 𝑦 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))))
109rexbidv 2375 . . 3 (𝑤 = 𝑦 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))))
11 breq1 3814 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑗))
12 uneq2 3132 . . . . . 6 (𝑤 = (𝑦 ∪ {𝑧}) → (𝐴𝑤) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
1312breq1d 3821 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐴𝑤) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗)))
1411, 13anbi12d 457 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗))))
1514rexbidv 2375 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗))))
16 breq1 3814 . . . . 5 (𝑤 = 𝐵 → (𝑤𝑗𝐵𝑗))
17 uneq2 3132 . . . . . 6 (𝑤 = 𝐵 → (𝐴𝑤) = (𝐴𝐵))
1817breq1d 3821 . . . . 5 (𝑤 = 𝐵 → ((𝐴𝑤) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))
1916, 18anbi12d 457 . . . 4 (𝑤 = 𝐵 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗))))
2019rexbidv 2375 . . 3 (𝑤 = 𝐵 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗))))
21 peano1 4372 . . . . 5 ∅ ∈ ω
2221a1i 9 . . . 4 (𝜑 → ∅ ∈ ω)
23 0ex 3931 . . . . . 6 ∅ ∈ V
2423enref 6412 . . . . 5 ∅ ≈ ∅
2524a1i 9 . . . 4 (𝜑 → ∅ ≈ ∅)
26 hashunlem.an . . . . 5 (𝜑𝐴𝑁)
27 un0 3299 . . . . . 6 (𝐴 ∪ ∅) = 𝐴
2827a1i 9 . . . . 5 (𝜑 → (𝐴 ∪ ∅) = 𝐴)
29 hashunlem.n . . . . . 6 (𝜑𝑁 ∈ ω)
30 nna0 6167 . . . . . 6 (𝑁 ∈ ω → (𝑁 +𝑜 ∅) = 𝑁)
3129, 30syl 14 . . . . 5 (𝜑 → (𝑁 +𝑜 ∅) = 𝑁)
3226, 28, 313brtr4d 3841 . . . 4 (𝜑 → (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 ∅))
33 breq2 3815 . . . . . 6 (𝑗 = ∅ → (∅ ≈ 𝑗 ↔ ∅ ≈ ∅))
34 oveq2 5599 . . . . . . 7 (𝑗 = ∅ → (𝑁 +𝑜 𝑗) = (𝑁 +𝑜 ∅))
3534breq2d 3823 . . . . . 6 (𝑗 = ∅ → ((𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 ∅)))
3633, 35anbi12d 457 . . . . 5 (𝑗 = ∅ → ((∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗)) ↔ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 ∅))))
3736rspcev 2712 . . . 4 ((∅ ∈ ω ∧ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 ∅))) → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗)))
3822, 25, 32, 37syl12anc 1168 . . 3 (𝜑 → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +𝑜 𝑗)))
39 peano2 4373 . . . . . . . 8 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
4039ad2antlr 473 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → suc 𝑗 ∈ ω)
41 simp-4r 509 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑦 ∈ Fin)
42 vex 2615 . . . . . . . . . 10 𝑧 ∈ V
4342a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧 ∈ V)
44 simprr 499 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → 𝑧 ∈ (𝐵𝑦))
4544ad2antrr 472 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧 ∈ (𝐵𝑦))
4645eldifbd 2996 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ¬ 𝑧𝑦)
4743, 46eldifd 2994 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧 ∈ (V ∖ 𝑦))
48 simplr 497 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑗 ∈ ω)
49 simprl 498 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑦𝑗)
50 fiunsnnn 6527 . . . . . . . 8 (((𝑦 ∈ Fin ∧ 𝑧 ∈ (V ∖ 𝑦)) ∧ (𝑗 ∈ ω ∧ 𝑦𝑗)) → (𝑦 ∪ {𝑧}) ≈ suc 𝑗)
5141, 47, 48, 49, 50syl22anc 1171 . . . . . . 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 3176 . . . . . . . . . . . 12 (𝑦𝐴) = (𝐴𝑦)
59 incom 3176 . . . . . . . . . . . . . 14 (𝐴𝐵) = (𝐵𝐴)
6059eqeq1i 2090 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
61 ssdisj 3321 . . . . . . . . . . . . 13 ((𝑦𝐵 ∧ (𝐵𝐴) = ∅) → (𝑦𝐴) = ∅)
6260, 61sylan2b 281 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝑦𝐴) = ∅)
6358, 62syl5eqr 2129 . . . . . . . . . . 11 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝐴𝑦) = ∅)
6455, 57, 63syl2anc 403 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴𝑦) = ∅)
65 unfidisj 6559 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ∧ (𝐴𝑦) = ∅) → (𝐴𝑦) ∈ Fin)
6653, 41, 64, 65syl3anc 1170 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴𝑦) ∈ Fin)
6745eldifad 2995 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧𝐵)
68 minel 3326 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (𝐴𝐵) = ∅) → ¬ 𝑧𝐴)
6967, 57, 68syl2anc 403 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ¬ 𝑧𝐴)
70 ioran 702 . . . . . . . . . . . 12 (¬ (𝑧𝐴𝑧𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
71 elun 3125 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
7270, 71xchnxbir 639 . . . . . . . . . . 11 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
7369, 46, 72sylanbrc 408 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ¬ 𝑧 ∈ (𝐴𝑦))
7443, 73eldifd 2994 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑧 ∈ (V ∖ (𝐴𝑦)))
7529ad4antr 478 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → 𝑁 ∈ ω)
76 nnacl 6173 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +𝑜 𝑗) ∈ ω)
7775, 48, 76syl2anc 403 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝑁 +𝑜 𝑗) ∈ ω)
78 simprr 499 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))
79 fiunsnnn 6527 . . . . . . . . 9 ((((𝐴𝑦) ∈ Fin ∧ 𝑧 ∈ (V ∖ (𝐴𝑦))) ∧ ((𝑁 +𝑜 𝑗) ∈ ω ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +𝑜 𝑗))
8066, 74, 77, 78, 79syl22anc 1171 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +𝑜 𝑗))
81 unass 3141 . . . . . . . . . 10 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
8281a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
8382eqcomd 2088 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ {𝑧}))
84 nnasuc 6169 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +𝑜 suc 𝑗) = suc (𝑁 +𝑜 𝑗))
8575, 48, 84syl2anc 403 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝑁 +𝑜 suc 𝑗) = suc (𝑁 +𝑜 𝑗))
8680, 83, 853brtr4d 3841 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 suc 𝑗))
87 breq2 3815 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝑦 ∪ {𝑧}) ≈ 𝑘 ↔ (𝑦 ∪ {𝑧}) ≈ suc 𝑗))
88 oveq2 5599 . . . . . . . . . 10 (𝑘 = suc 𝑗 → (𝑁 +𝑜 𝑘) = (𝑁 +𝑜 suc 𝑗))
8988breq2d 3823 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 suc 𝑗)))
9087, 89anbi12d 457 . . . . . . . 8 (𝑘 = suc 𝑗 → (((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)) ↔ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 suc 𝑗))))
9190rspcev 2712 . . . . . . 7 ((suc 𝑗 ∈ ω ∧ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 suc 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)))
9240, 51, 86, 91syl12anc 1168 . . . . . 6 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)))
9392ex 113 . . . . 5 ((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) → ((𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘))))
9493rexlimdva 2483 . . . 4 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘))))
95 breq2 3815 . . . . . 6 (𝑗 = 𝑘 → ((𝑦 ∪ {𝑧}) ≈ 𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑘))
96 oveq2 5599 . . . . . . 7 (𝑗 = 𝑘 → (𝑁 +𝑜 𝑗) = (𝑁 +𝑜 𝑘))
9796breq2d 3823 . . . . . 6 (𝑗 = 𝑘 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)))
9895, 97anbi12d 457 . . . . 5 (𝑗 = 𝑘 → (((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘))))
9998cbvrexv 2584 . . . 4 (∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗)) ↔ ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑘)))
10094, 99syl6ibr 160 . . 3 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +𝑜 𝑗)) → ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +𝑜 𝑗))))
101 hashunlem.b . . 3 (𝜑𝐵 ∈ Fin)
1025, 10, 15, 20, 38, 100, 101findcard2sd 6538 . 2 (𝜑 → ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))
103 simprrr 507 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗))
104 hashunlem.bm . . . . . . 7 (𝜑𝐵𝑀)
105104ensymd 6430 . . . . . 6 (𝜑𝑀𝐵)
106 simprrl 506 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → 𝐵𝑗)
107 entr 6431 . . . . . 6 ((𝑀𝐵𝐵𝑗) → 𝑀𝑗)
108105, 106, 107syl2an2r 560 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → 𝑀𝑗)
109 hashunlem.m . . . . . 6 (𝜑𝑀 ∈ ω)
110 simprl 498 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → 𝑗 ∈ ω)
111 nneneq 6503 . . . . . 6 ((𝑀 ∈ ω ∧ 𝑗 ∈ ω) → (𝑀𝑗𝑀 = 𝑗))
112109, 110, 111syl2an2r 560 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → (𝑀𝑗𝑀 = 𝑗))
113108, 112mpbid 145 . . . 4 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → 𝑀 = 𝑗)
114113oveq2d 5607 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → (𝑁 +𝑜 𝑀) = (𝑁 +𝑜 𝑗))
115103, 114breqtrrd 3837 . 2 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +𝑜 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +𝑜 𝑀))
116102, 115rexlimddv 2487 1 (𝜑 → (𝐴𝐵) ≈ (𝑁 +𝑜 𝑀))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662   = wceq 1285  wcel 1434  wrex 2354  Vcvv 2612  cdif 2981  cun 2982  cin 2983  wss 2984  c0 3269  {csn 3422   class class class wbr 3811  suc csuc 4156  ωcom 4368  (class class class)co 5591   +𝑜 coa 6110  cen 6385  Fincfn 6387
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3919  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 4000  ax-un 4224  ax-setind 4316  ax-iinf 4366
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-if 3374  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-tr 3902  df-id 4084  df-iord 4157  df-on 4159  df-suc 4162  df-iom 4369  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-res 4413  df-ima 4414  df-iota 4934  df-fun 4971  df-fn 4972  df-f 4973  df-f1 4974  df-fo 4975  df-f1o 4976  df-fv 4977  df-ov 5594  df-oprab 5595  df-mpt2 5596  df-1st 5846  df-2nd 5847  df-recs 6002  df-irdg 6067  df-1o 6113  df-oadd 6117  df-er 6222  df-en 6388  df-fin 6390
This theorem is referenced by:  hashun  10048
  Copyright terms: Public domain W3C validator