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

Theorem hashunlem 10815
Description: Lemma for hashun 10816. 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 (𝜑 → (𝐴𝐵) ≈ (𝑁 +o 𝑀))

Proof of Theorem hashunlem
Dummy variables 𝑗 𝑤 𝑘 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 4021 . . . . 5 (𝑤 = ∅ → (𝑤𝑗 ↔ ∅ ≈ 𝑗))
2 uneq2 3298 . . . . . 6 (𝑤 = ∅ → (𝐴𝑤) = (𝐴 ∪ ∅))
32breq1d 4028 . . . . 5 (𝑤 = ∅ → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
41, 3anbi12d 473 . . . 4 (𝑤 = ∅ → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗))))
54rexbidv 2491 . . 3 (𝑤 = ∅ → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗))))
6 breq1 4021 . . . . 5 (𝑤 = 𝑦 → (𝑤𝑗𝑦𝑗))
7 uneq2 3298 . . . . . 6 (𝑤 = 𝑦 → (𝐴𝑤) = (𝐴𝑦))
87breq1d 4028 . . . . 5 (𝑤 = 𝑦 → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴𝑦) ≈ (𝑁 +o 𝑗)))
96, 8anbi12d 473 . . . 4 (𝑤 = 𝑦 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))))
109rexbidv 2491 . . 3 (𝑤 = 𝑦 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))))
11 breq1 4021 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑗))
12 uneq2 3298 . . . . . 6 (𝑤 = (𝑦 ∪ {𝑧}) → (𝐴𝑤) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
1312breq1d 4028 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)))
1411, 13anbi12d 473 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
1514rexbidv 2491 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
16 breq1 4021 . . . . 5 (𝑤 = 𝐵 → (𝑤𝑗𝐵𝑗))
17 uneq2 3298 . . . . . 6 (𝑤 = 𝐵 → (𝐴𝑤) = (𝐴𝐵))
1817breq1d 4028 . . . . 5 (𝑤 = 𝐵 → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))
1916, 18anbi12d 473 . . . 4 (𝑤 = 𝐵 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗))))
2019rexbidv 2491 . . 3 (𝑤 = 𝐵 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗))))
21 peano1 4611 . . . . 5 ∅ ∈ ω
2221a1i 9 . . . 4 (𝜑 → ∅ ∈ ω)
23 0ex 4145 . . . . . 6 ∅ ∈ V
2423enref 6790 . . . . 5 ∅ ≈ ∅
2524a1i 9 . . . 4 (𝜑 → ∅ ≈ ∅)
26 hashunlem.an . . . . 5 (𝜑𝐴𝑁)
27 un0 3471 . . . . . 6 (𝐴 ∪ ∅) = 𝐴
2827a1i 9 . . . . 5 (𝜑 → (𝐴 ∪ ∅) = 𝐴)
29 hashunlem.n . . . . . 6 (𝜑𝑁 ∈ ω)
30 nna0 6498 . . . . . 6 (𝑁 ∈ ω → (𝑁 +o ∅) = 𝑁)
3129, 30syl 14 . . . . 5 (𝜑 → (𝑁 +o ∅) = 𝑁)
3226, 28, 313brtr4d 4050 . . . 4 (𝜑 → (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))
33 breq2 4022 . . . . . 6 (𝑗 = ∅ → (∅ ≈ 𝑗 ↔ ∅ ≈ ∅))
34 oveq2 5903 . . . . . . 7 (𝑗 = ∅ → (𝑁 +o 𝑗) = (𝑁 +o ∅))
3534breq2d 4030 . . . . . 6 (𝑗 = ∅ → ((𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅)))
3633, 35anbi12d 473 . . . . 5 (𝑗 = ∅ → ((∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)) ↔ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))))
3736rspcev 2856 . . . 4 ((∅ ∈ ω ∧ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))) → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
3822, 25, 32, 37syl12anc 1247 . . 3 (𝜑 → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
39 peano2 4612 . . . . . . . 8 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
4039ad2antlr 489 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → suc 𝑗 ∈ ω)
41 simp-4r 542 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑦 ∈ Fin)
42 vex 2755 . . . . . . . . . 10 𝑧 ∈ V
4342a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ V)
44 simprr 531 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → 𝑧 ∈ (𝐵𝑦))
4544ad2antrr 488 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (𝐵𝑦))
4645eldifbd 3156 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧𝑦)
4743, 46eldifd 3154 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (V ∖ 𝑦))
48 simplr 528 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑗 ∈ ω)
49 simprl 529 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑦𝑗)
50 fiunsnnn 6908 . . . . . . . 8 (((𝑦 ∈ Fin ∧ 𝑧 ∈ (V ∖ 𝑦)) ∧ (𝑗 ∈ ω ∧ 𝑦𝑗)) → (𝑦 ∪ {𝑧}) ≈ suc 𝑗)
5141, 47, 48, 49, 50syl22anc 1250 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝑦 ∪ {𝑧}) ≈ suc 𝑗)
52 hashunlem.a . . . . . . . . . . 11 (𝜑𝐴 ∈ Fin)
5352ad4antr 494 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝐴 ∈ Fin)
54 simprl 529 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → 𝑦𝐵)
5554ad2antrr 488 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑦𝐵)
56 hashunlem.disj . . . . . . . . . . . 12 (𝜑 → (𝐴𝐵) = ∅)
5756ad4antr 494 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝐵) = ∅)
58 incom 3342 . . . . . . . . . . . 12 (𝑦𝐴) = (𝐴𝑦)
59 incom 3342 . . . . . . . . . . . . . 14 (𝐴𝐵) = (𝐵𝐴)
6059eqeq1i 2197 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
61 ssdisj 3494 . . . . . . . . . . . . 13 ((𝑦𝐵 ∧ (𝐵𝐴) = ∅) → (𝑦𝐴) = ∅)
6260, 61sylan2b 287 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝑦𝐴) = ∅)
6358, 62eqtr3id 2236 . . . . . . . . . . 11 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝐴𝑦) = ∅)
6455, 57, 63syl2anc 411 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) = ∅)
65 unfidisj 6949 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ∧ (𝐴𝑦) = ∅) → (𝐴𝑦) ∈ Fin)
6653, 41, 64, 65syl3anc 1249 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) ∈ Fin)
6745eldifad 3155 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧𝐵)
68 minel 3499 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (𝐴𝐵) = ∅) → ¬ 𝑧𝐴)
6967, 57, 68syl2anc 411 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧𝐴)
70 ioran 753 . . . . . . . . . . . 12 (¬ (𝑧𝐴𝑧𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
71 elun 3291 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
7270, 71xchnxbir 682 . . . . . . . . . . 11 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
7369, 46, 72sylanbrc 417 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧 ∈ (𝐴𝑦))
7443, 73eldifd 3154 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (V ∖ (𝐴𝑦)))
7529ad4antr 494 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑁 ∈ ω)
76 nnacl 6504 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +o 𝑗) ∈ ω)
7775, 48, 76syl2anc 411 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝑁 +o 𝑗) ∈ ω)
78 simprr 531 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) ≈ (𝑁 +o 𝑗))
79 fiunsnnn 6908 . . . . . . . . 9 ((((𝐴𝑦) ∈ Fin ∧ 𝑧 ∈ (V ∖ (𝐴𝑦))) ∧ ((𝑁 +o 𝑗) ∈ ω ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +o 𝑗))
8066, 74, 77, 78, 79syl22anc 1250 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +o 𝑗))
81 unass 3307 . . . . . . . . . 10 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
8281a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
8382eqcomd 2195 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ {𝑧}))
84 nnasuc 6500 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +o suc 𝑗) = suc (𝑁 +o 𝑗))
8575, 48, 84syl2anc 411 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝑁 +o suc 𝑗) = suc (𝑁 +o 𝑗))
8680, 83, 853brtr4d 4050 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))
87 breq2 4022 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝑦 ∪ {𝑧}) ≈ 𝑘 ↔ (𝑦 ∪ {𝑧}) ≈ suc 𝑗))
88 oveq2 5903 . . . . . . . . . 10 (𝑘 = suc 𝑗 → (𝑁 +o 𝑘) = (𝑁 +o suc 𝑗))
8988breq2d 4030 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗)))
9087, 89anbi12d 473 . . . . . . . 8 (𝑘 = suc 𝑗 → (((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)) ↔ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))))
9190rspcev 2856 . . . . . . 7 ((suc 𝑗 ∈ ω ∧ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9240, 51, 86, 91syl12anc 1247 . . . . . 6 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9392ex 115 . . . . 5 ((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) → ((𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
9493rexlimdva 2607 . . . 4 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
95 breq2 4022 . . . . . 6 (𝑗 = 𝑘 → ((𝑦 ∪ {𝑧}) ≈ 𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑘))
96 oveq2 5903 . . . . . . 7 (𝑗 = 𝑘 → (𝑁 +o 𝑗) = (𝑁 +o 𝑘))
9796breq2d 4030 . . . . . 6 (𝑗 = 𝑘 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9895, 97anbi12d 473 . . . . 5 (𝑗 = 𝑘 → (((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
9998cbvrexv 2719 . . . 4 (∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
10094, 99imbitrrdi 162 . . 3 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
101 hashunlem.b . . 3 (𝜑𝐵 ∈ Fin)
1025, 10, 15, 20, 38, 100, 101findcard2sd 6919 . 2 (𝜑 → ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))
103 simprrr 540 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +o 𝑗))
104 hashunlem.bm . . . . . . 7 (𝜑𝐵𝑀)
105104ensymd 6808 . . . . . 6 (𝜑𝑀𝐵)
106 simprrl 539 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝐵𝑗)
107 entr 6809 . . . . . 6 ((𝑀𝐵𝐵𝑗) → 𝑀𝑗)
108105, 106, 107syl2an2r 595 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑀𝑗)
109 hashunlem.m . . . . . 6 (𝜑𝑀 ∈ ω)
110 simprl 529 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑗 ∈ ω)
111 nneneq 6884 . . . . . 6 ((𝑀 ∈ ω ∧ 𝑗 ∈ ω) → (𝑀𝑗𝑀 = 𝑗))
112109, 110, 111syl2an2r 595 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝑀𝑗𝑀 = 𝑗))
113108, 112mpbid 147 . . . 4 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑀 = 𝑗)
114113oveq2d 5911 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝑁 +o 𝑀) = (𝑁 +o 𝑗))
115103, 114breqtrrd 4046 . 2 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +o 𝑀))
116102, 115rexlimddv 2612 1 (𝜑 → (𝐴𝐵) ≈ (𝑁 +o 𝑀))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709   = wceq 1364  wcel 2160  wrex 2469  Vcvv 2752  cdif 3141  cun 3142  cin 3143  wss 3144  c0 3437  {csn 3607   class class class wbr 4018  suc csuc 4383  ωcom 4607  (class class class)co 5895   +o coa 6437  cen 6763  Fincfn 6765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-iord 4384  df-on 4386  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-ov 5898  df-oprab 5899  df-mpo 5900  df-1st 6164  df-2nd 6165  df-recs 6329  df-irdg 6394  df-1o 6440  df-oadd 6444  df-er 6558  df-en 6766  df-fin 6768
This theorem is referenced by:  hashun  10816
  Copyright terms: Public domain W3C validator