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

Theorem hashunlem 10391
Description: Lemma for hashun 10392. 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 3878 . . . . 5 (𝑤 = ∅ → (𝑤𝑗 ↔ ∅ ≈ 𝑗))
2 uneq2 3171 . . . . . 6 (𝑤 = ∅ → (𝐴𝑤) = (𝐴 ∪ ∅))
32breq1d 3885 . . . . 5 (𝑤 = ∅ → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
41, 3anbi12d 460 . . . 4 (𝑤 = ∅ → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗))))
54rexbidv 2397 . . 3 (𝑤 = ∅ → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗))))
6 breq1 3878 . . . . 5 (𝑤 = 𝑦 → (𝑤𝑗𝑦𝑗))
7 uneq2 3171 . . . . . 6 (𝑤 = 𝑦 → (𝐴𝑤) = (𝐴𝑦))
87breq1d 3885 . . . . 5 (𝑤 = 𝑦 → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴𝑦) ≈ (𝑁 +o 𝑗)))
96, 8anbi12d 460 . . . 4 (𝑤 = 𝑦 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))))
109rexbidv 2397 . . 3 (𝑤 = 𝑦 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))))
11 breq1 3878 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑗))
12 uneq2 3171 . . . . . 6 (𝑤 = (𝑦 ∪ {𝑧}) → (𝐴𝑤) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
1312breq1d 3885 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)))
1411, 13anbi12d 460 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
1514rexbidv 2397 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
16 breq1 3878 . . . . 5 (𝑤 = 𝐵 → (𝑤𝑗𝐵𝑗))
17 uneq2 3171 . . . . . 6 (𝑤 = 𝐵 → (𝐴𝑤) = (𝐴𝐵))
1817breq1d 3885 . . . . 5 (𝑤 = 𝐵 → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))
1916, 18anbi12d 460 . . . 4 (𝑤 = 𝐵 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗))))
2019rexbidv 2397 . . 3 (𝑤 = 𝐵 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗))))
21 peano1 4446 . . . . 5 ∅ ∈ ω
2221a1i 9 . . . 4 (𝜑 → ∅ ∈ ω)
23 0ex 3995 . . . . . 6 ∅ ∈ V
2423enref 6589 . . . . 5 ∅ ≈ ∅
2524a1i 9 . . . 4 (𝜑 → ∅ ≈ ∅)
26 hashunlem.an . . . . 5 (𝜑𝐴𝑁)
27 un0 3343 . . . . . 6 (𝐴 ∪ ∅) = 𝐴
2827a1i 9 . . . . 5 (𝜑 → (𝐴 ∪ ∅) = 𝐴)
29 hashunlem.n . . . . . 6 (𝜑𝑁 ∈ ω)
30 nna0 6300 . . . . . 6 (𝑁 ∈ ω → (𝑁 +o ∅) = 𝑁)
3129, 30syl 14 . . . . 5 (𝜑 → (𝑁 +o ∅) = 𝑁)
3226, 28, 313brtr4d 3905 . . . 4 (𝜑 → (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))
33 breq2 3879 . . . . . 6 (𝑗 = ∅ → (∅ ≈ 𝑗 ↔ ∅ ≈ ∅))
34 oveq2 5714 . . . . . . 7 (𝑗 = ∅ → (𝑁 +o 𝑗) = (𝑁 +o ∅))
3534breq2d 3887 . . . . . 6 (𝑗 = ∅ → ((𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅)))
3633, 35anbi12d 460 . . . . 5 (𝑗 = ∅ → ((∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)) ↔ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))))
3736rspcev 2744 . . . 4 ((∅ ∈ ω ∧ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))) → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
3822, 25, 32, 37syl12anc 1182 . . 3 (𝜑 → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
39 peano2 4447 . . . . . . . 8 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
4039ad2antlr 476 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → suc 𝑗 ∈ ω)
41 simp-4r 512 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑦 ∈ Fin)
42 vex 2644 . . . . . . . . . 10 𝑧 ∈ V
4342a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ V)
44 simprr 502 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → 𝑧 ∈ (𝐵𝑦))
4544ad2antrr 475 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (𝐵𝑦))
4645eldifbd 3033 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧𝑦)
4743, 46eldifd 3031 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (V ∖ 𝑦))
48 simplr 500 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑗 ∈ ω)
49 simprl 501 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑦𝑗)
50 fiunsnnn 6704 . . . . . . . 8 (((𝑦 ∈ Fin ∧ 𝑧 ∈ (V ∖ 𝑦)) ∧ (𝑗 ∈ ω ∧ 𝑦𝑗)) → (𝑦 ∪ {𝑧}) ≈ suc 𝑗)
5141, 47, 48, 49, 50syl22anc 1185 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝑦 ∪ {𝑧}) ≈ suc 𝑗)
52 hashunlem.a . . . . . . . . . . 11 (𝜑𝐴 ∈ Fin)
5352ad4antr 481 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝐴 ∈ Fin)
54 simprl 501 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → 𝑦𝐵)
5554ad2antrr 475 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑦𝐵)
56 hashunlem.disj . . . . . . . . . . . 12 (𝜑 → (𝐴𝐵) = ∅)
5756ad4antr 481 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝐵) = ∅)
58 incom 3215 . . . . . . . . . . . 12 (𝑦𝐴) = (𝐴𝑦)
59 incom 3215 . . . . . . . . . . . . . 14 (𝐴𝐵) = (𝐵𝐴)
6059eqeq1i 2107 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
61 ssdisj 3366 . . . . . . . . . . . . 13 ((𝑦𝐵 ∧ (𝐵𝐴) = ∅) → (𝑦𝐴) = ∅)
6260, 61sylan2b 283 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝑦𝐴) = ∅)
6358, 62syl5eqr 2146 . . . . . . . . . . 11 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝐴𝑦) = ∅)
6455, 57, 63syl2anc 406 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) = ∅)
65 unfidisj 6739 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ∧ (𝐴𝑦) = ∅) → (𝐴𝑦) ∈ Fin)
6653, 41, 64, 65syl3anc 1184 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) ∈ Fin)
6745eldifad 3032 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧𝐵)
68 minel 3371 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (𝐴𝐵) = ∅) → ¬ 𝑧𝐴)
6967, 57, 68syl2anc 406 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧𝐴)
70 ioran 710 . . . . . . . . . . . 12 (¬ (𝑧𝐴𝑧𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
71 elun 3164 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
7270, 71xchnxbir 647 . . . . . . . . . . 11 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
7369, 46, 72sylanbrc 411 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧 ∈ (𝐴𝑦))
7443, 73eldifd 3031 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (V ∖ (𝐴𝑦)))
7529ad4antr 481 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑁 ∈ ω)
76 nnacl 6306 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +o 𝑗) ∈ ω)
7775, 48, 76syl2anc 406 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝑁 +o 𝑗) ∈ ω)
78 simprr 502 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) ≈ (𝑁 +o 𝑗))
79 fiunsnnn 6704 . . . . . . . . 9 ((((𝐴𝑦) ∈ Fin ∧ 𝑧 ∈ (V ∖ (𝐴𝑦))) ∧ ((𝑁 +o 𝑗) ∈ ω ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +o 𝑗))
8066, 74, 77, 78, 79syl22anc 1185 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +o 𝑗))
81 unass 3180 . . . . . . . . . 10 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
8281a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
8382eqcomd 2105 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ {𝑧}))
84 nnasuc 6302 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +o suc 𝑗) = suc (𝑁 +o 𝑗))
8575, 48, 84syl2anc 406 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝑁 +o suc 𝑗) = suc (𝑁 +o 𝑗))
8680, 83, 853brtr4d 3905 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))
87 breq2 3879 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝑦 ∪ {𝑧}) ≈ 𝑘 ↔ (𝑦 ∪ {𝑧}) ≈ suc 𝑗))
88 oveq2 5714 . . . . . . . . . 10 (𝑘 = suc 𝑗 → (𝑁 +o 𝑘) = (𝑁 +o suc 𝑗))
8988breq2d 3887 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗)))
9087, 89anbi12d 460 . . . . . . . 8 (𝑘 = suc 𝑗 → (((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)) ↔ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))))
9190rspcev 2744 . . . . . . 7 ((suc 𝑗 ∈ ω ∧ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9240, 51, 86, 91syl12anc 1182 . . . . . 6 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9392ex 114 . . . . 5 ((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) → ((𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
9493rexlimdva 2508 . . . 4 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
95 breq2 3879 . . . . . 6 (𝑗 = 𝑘 → ((𝑦 ∪ {𝑧}) ≈ 𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑘))
96 oveq2 5714 . . . . . . 7 (𝑗 = 𝑘 → (𝑁 +o 𝑗) = (𝑁 +o 𝑘))
9796breq2d 3887 . . . . . 6 (𝑗 = 𝑘 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9895, 97anbi12d 460 . . . . 5 (𝑗 = 𝑘 → (((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
9998cbvrexv 2613 . . . 4 (∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
10094, 99syl6ibr 161 . . 3 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
101 hashunlem.b . . 3 (𝜑𝐵 ∈ Fin)
1025, 10, 15, 20, 38, 100, 101findcard2sd 6715 . 2 (𝜑 → ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))
103 simprrr 510 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +o 𝑗))
104 hashunlem.bm . . . . . . 7 (𝜑𝐵𝑀)
105104ensymd 6607 . . . . . 6 (𝜑𝑀𝐵)
106 simprrl 509 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝐵𝑗)
107 entr 6608 . . . . . 6 ((𝑀𝐵𝐵𝑗) → 𝑀𝑗)
108105, 106, 107syl2an2r 565 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑀𝑗)
109 hashunlem.m . . . . . 6 (𝜑𝑀 ∈ ω)
110 simprl 501 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑗 ∈ ω)
111 nneneq 6680 . . . . . 6 ((𝑀 ∈ ω ∧ 𝑗 ∈ ω) → (𝑀𝑗𝑀 = 𝑗))
112109, 110, 111syl2an2r 565 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝑀𝑗𝑀 = 𝑗))
113108, 112mpbid 146 . . . 4 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑀 = 𝑗)
114113oveq2d 5722 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝑁 +o 𝑀) = (𝑁 +o 𝑗))
115103, 114breqtrrd 3901 . 2 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +o 𝑀))
116102, 115rexlimddv 2513 1 (𝜑 → (𝐴𝐵) ≈ (𝑁 +o 𝑀))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 670   = wceq 1299  wcel 1448  wrex 2376  Vcvv 2641  cdif 3018  cun 3019  cin 3020  wss 3021  c0 3310  {csn 3474   class class class wbr 3875  suc csuc 4225  ωcom 4442  (class class class)co 5706   +o coa 6240  cen 6562  Fincfn 6564
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-coll 3983  ax-sep 3986  ax-nul 3994  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-iinf 4440
This theorem depends on definitions:  df-bi 116  df-dc 787  df-3or 931  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-csb 2956  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-nul 3311  df-if 3422  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-int 3719  df-iun 3762  df-br 3876  df-opab 3930  df-mpt 3931  df-tr 3967  df-id 4153  df-iord 4226  df-on 4228  df-suc 4231  df-iom 4443  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066  df-fv 5067  df-ov 5709  df-oprab 5710  df-mpo 5711  df-1st 5969  df-2nd 5970  df-recs 6132  df-irdg 6197  df-1o 6243  df-oadd 6247  df-er 6359  df-en 6565  df-fin 6567
This theorem is referenced by:  hashun  10392
  Copyright terms: Public domain W3C validator