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

Theorem hashunlem 10768
Description: Lemma for hashun 10769. 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 4003 . . . . 5 (𝑤 = ∅ → (𝑤𝑗 ↔ ∅ ≈ 𝑗))
2 uneq2 3283 . . . . . 6 (𝑤 = ∅ → (𝐴𝑤) = (𝐴 ∪ ∅))
32breq1d 4010 . . . . 5 (𝑤 = ∅ → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
41, 3anbi12d 473 . . . 4 (𝑤 = ∅ → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗))))
54rexbidv 2478 . . 3 (𝑤 = ∅ → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗))))
6 breq1 4003 . . . . 5 (𝑤 = 𝑦 → (𝑤𝑗𝑦𝑗))
7 uneq2 3283 . . . . . 6 (𝑤 = 𝑦 → (𝐴𝑤) = (𝐴𝑦))
87breq1d 4010 . . . . 5 (𝑤 = 𝑦 → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴𝑦) ≈ (𝑁 +o 𝑗)))
96, 8anbi12d 473 . . . 4 (𝑤 = 𝑦 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))))
109rexbidv 2478 . . 3 (𝑤 = 𝑦 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))))
11 breq1 4003 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑗))
12 uneq2 3283 . . . . . 6 (𝑤 = (𝑦 ∪ {𝑧}) → (𝐴𝑤) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
1312breq1d 4010 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)))
1411, 13anbi12d 473 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
1514rexbidv 2478 . . 3 (𝑤 = (𝑦 ∪ {𝑧}) → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
16 breq1 4003 . . . . 5 (𝑤 = 𝐵 → (𝑤𝑗𝐵𝑗))
17 uneq2 3283 . . . . . 6 (𝑤 = 𝐵 → (𝐴𝑤) = (𝐴𝐵))
1817breq1d 4010 . . . . 5 (𝑤 = 𝐵 → ((𝐴𝑤) ≈ (𝑁 +o 𝑗) ↔ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))
1916, 18anbi12d 473 . . . 4 (𝑤 = 𝐵 → ((𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗))))
2019rexbidv 2478 . . 3 (𝑤 = 𝐵 → (∃𝑗 ∈ ω (𝑤𝑗 ∧ (𝐴𝑤) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗))))
21 peano1 4590 . . . . 5 ∅ ∈ ω
2221a1i 9 . . . 4 (𝜑 → ∅ ∈ ω)
23 0ex 4127 . . . . . 6 ∅ ∈ V
2423enref 6759 . . . . 5 ∅ ≈ ∅
2524a1i 9 . . . 4 (𝜑 → ∅ ≈ ∅)
26 hashunlem.an . . . . 5 (𝜑𝐴𝑁)
27 un0 3456 . . . . . 6 (𝐴 ∪ ∅) = 𝐴
2827a1i 9 . . . . 5 (𝜑 → (𝐴 ∪ ∅) = 𝐴)
29 hashunlem.n . . . . . 6 (𝜑𝑁 ∈ ω)
30 nna0 6469 . . . . . 6 (𝑁 ∈ ω → (𝑁 +o ∅) = 𝑁)
3129, 30syl 14 . . . . 5 (𝜑 → (𝑁 +o ∅) = 𝑁)
3226, 28, 313brtr4d 4032 . . . 4 (𝜑 → (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))
33 breq2 4004 . . . . . 6 (𝑗 = ∅ → (∅ ≈ 𝑗 ↔ ∅ ≈ ∅))
34 oveq2 5877 . . . . . . 7 (𝑗 = ∅ → (𝑁 +o 𝑗) = (𝑁 +o ∅))
3534breq2d 4012 . . . . . 6 (𝑗 = ∅ → ((𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅)))
3633, 35anbi12d 473 . . . . 5 (𝑗 = ∅ → ((∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)) ↔ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))))
3736rspcev 2841 . . . 4 ((∅ ∈ ω ∧ (∅ ≈ ∅ ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o ∅))) → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
3822, 25, 32, 37syl12anc 1236 . . 3 (𝜑 → ∃𝑗 ∈ ω (∅ ≈ 𝑗 ∧ (𝐴 ∪ ∅) ≈ (𝑁 +o 𝑗)))
39 peano2 4591 . . . . . . . 8 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
4039ad2antlr 489 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → suc 𝑗 ∈ ω)
41 simp-4r 542 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑦 ∈ Fin)
42 vex 2740 . . . . . . . . . 10 𝑧 ∈ V
4342a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ V)
44 simprr 531 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → 𝑧 ∈ (𝐵𝑦))
4544ad2antrr 488 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (𝐵𝑦))
4645eldifbd 3141 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧𝑦)
4743, 46eldifd 3139 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (V ∖ 𝑦))
48 simplr 528 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑗 ∈ ω)
49 simprl 529 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑦𝑗)
50 fiunsnnn 6875 . . . . . . . 8 (((𝑦 ∈ Fin ∧ 𝑧 ∈ (V ∖ 𝑦)) ∧ (𝑗 ∈ ω ∧ 𝑦𝑗)) → (𝑦 ∪ {𝑧}) ≈ suc 𝑗)
5141, 47, 48, 49, 50syl22anc 1239 . . . . . . 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 3327 . . . . . . . . . . . 12 (𝑦𝐴) = (𝐴𝑦)
59 incom 3327 . . . . . . . . . . . . . 14 (𝐴𝐵) = (𝐵𝐴)
6059eqeq1i 2185 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
61 ssdisj 3479 . . . . . . . . . . . . 13 ((𝑦𝐵 ∧ (𝐵𝐴) = ∅) → (𝑦𝐴) = ∅)
6260, 61sylan2b 287 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝑦𝐴) = ∅)
6358, 62eqtr3id 2224 . . . . . . . . . . 11 ((𝑦𝐵 ∧ (𝐴𝐵) = ∅) → (𝐴𝑦) = ∅)
6455, 57, 63syl2anc 411 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) = ∅)
65 unfidisj 6915 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ∧ (𝐴𝑦) = ∅) → (𝐴𝑦) ∈ Fin)
6653, 41, 64, 65syl3anc 1238 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) ∈ Fin)
6745eldifad 3140 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧𝐵)
68 minel 3484 . . . . . . . . . . . 12 ((𝑧𝐵 ∧ (𝐴𝐵) = ∅) → ¬ 𝑧𝐴)
6967, 57, 68syl2anc 411 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧𝐴)
70 ioran 752 . . . . . . . . . . . 12 (¬ (𝑧𝐴𝑧𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
71 elun 3276 . . . . . . . . . . . 12 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
7270, 71xchnxbir 681 . . . . . . . . . . 11 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
7369, 46, 72sylanbrc 417 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ¬ 𝑧 ∈ (𝐴𝑦))
7443, 73eldifd 3139 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑧 ∈ (V ∖ (𝐴𝑦)))
7529ad4antr 494 . . . . . . . . . 10 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → 𝑁 ∈ ω)
76 nnacl 6475 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +o 𝑗) ∈ ω)
7775, 48, 76syl2anc 411 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝑁 +o 𝑗) ∈ ω)
78 simprr 531 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴𝑦) ≈ (𝑁 +o 𝑗))
79 fiunsnnn 6875 . . . . . . . . 9 ((((𝐴𝑦) ∈ Fin ∧ 𝑧 ∈ (V ∖ (𝐴𝑦))) ∧ ((𝑁 +o 𝑗) ∈ ω ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +o 𝑗))
8066, 74, 77, 78, 79syl22anc 1239 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) ≈ suc (𝑁 +o 𝑗))
81 unass 3292 . . . . . . . . . 10 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
8281a1i 9 . . . . . . . . 9 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
8382eqcomd 2183 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ {𝑧}))
84 nnasuc 6471 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑁 +o suc 𝑗) = suc (𝑁 +o 𝑗))
8575, 48, 84syl2anc 411 . . . . . . . 8 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝑁 +o suc 𝑗) = suc (𝑁 +o 𝑗))
8680, 83, 853brtr4d 4032 . . . . . . 7 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))
87 breq2 4004 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝑦 ∪ {𝑧}) ≈ 𝑘 ↔ (𝑦 ∪ {𝑧}) ≈ suc 𝑗))
88 oveq2 5877 . . . . . . . . . 10 (𝑘 = suc 𝑗 → (𝑁 +o 𝑘) = (𝑁 +o suc 𝑗))
8988breq2d 4012 . . . . . . . . 9 (𝑘 = suc 𝑗 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗)))
9087, 89anbi12d 473 . . . . . . . 8 (𝑘 = suc 𝑗 → (((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)) ↔ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))))
9190rspcev 2841 . . . . . . 7 ((suc 𝑗 ∈ ω ∧ ((𝑦 ∪ {𝑧}) ≈ suc 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o suc 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9240, 51, 86, 91syl12anc 1236 . . . . . 6 (((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) ∧ (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗))) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9392ex 115 . . . . 5 ((((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) ∧ 𝑗 ∈ ω) → ((𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
9493rexlimdva 2594 . . . 4 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
95 breq2 4004 . . . . . 6 (𝑗 = 𝑘 → ((𝑦 ∪ {𝑧}) ≈ 𝑗 ↔ (𝑦 ∪ {𝑧}) ≈ 𝑘))
96 oveq2 5877 . . . . . . 7 (𝑗 = 𝑘 → (𝑁 +o 𝑗) = (𝑁 +o 𝑘))
9796breq2d 4012 . . . . . 6 (𝑗 = 𝑘 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗) ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
9895, 97anbi12d 473 . . . . 5 (𝑗 = 𝑘 → (((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)) ↔ ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘))))
9998cbvrexv 2704 . . . 4 (∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗)) ↔ ∃𝑘 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑘 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑘)))
10094, 99syl6ibr 162 . . 3 (((𝜑𝑦 ∈ Fin) ∧ (𝑦𝐵𝑧 ∈ (𝐵𝑦))) → (∃𝑗 ∈ ω (𝑦𝑗 ∧ (𝐴𝑦) ≈ (𝑁 +o 𝑗)) → ∃𝑗 ∈ ω ((𝑦 ∪ {𝑧}) ≈ 𝑗 ∧ (𝐴 ∪ (𝑦 ∪ {𝑧})) ≈ (𝑁 +o 𝑗))))
101 hashunlem.b . . 3 (𝜑𝐵 ∈ Fin)
1025, 10, 15, 20, 38, 100, 101findcard2sd 6886 . 2 (𝜑 → ∃𝑗 ∈ ω (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))
103 simprrr 540 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +o 𝑗))
104 hashunlem.bm . . . . . . 7 (𝜑𝐵𝑀)
105104ensymd 6777 . . . . . 6 (𝜑𝑀𝐵)
106 simprrl 539 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝐵𝑗)
107 entr 6778 . . . . . 6 ((𝑀𝐵𝐵𝑗) → 𝑀𝑗)
108105, 106, 107syl2an2r 595 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑀𝑗)
109 hashunlem.m . . . . . 6 (𝜑𝑀 ∈ ω)
110 simprl 529 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑗 ∈ ω)
111 nneneq 6851 . . . . . 6 ((𝑀 ∈ ω ∧ 𝑗 ∈ ω) → (𝑀𝑗𝑀 = 𝑗))
112109, 110, 111syl2an2r 595 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝑀𝑗𝑀 = 𝑗))
113108, 112mpbid 147 . . . 4 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → 𝑀 = 𝑗)
114113oveq2d 5885 . . 3 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝑁 +o 𝑀) = (𝑁 +o 𝑗))
115103, 114breqtrrd 4028 . 2 ((𝜑 ∧ (𝑗 ∈ ω ∧ (𝐵𝑗 ∧ (𝐴𝐵) ≈ (𝑁 +o 𝑗)))) → (𝐴𝐵) ≈ (𝑁 +o 𝑀))
116102, 115rexlimddv 2599 1 (𝜑 → (𝐴𝐵) ≈ (𝑁 +o 𝑀))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708   = wceq 1353  wcel 2148  wrex 2456  Vcvv 2737  cdif 3126  cun 3127  cin 3128  wss 3129  c0 3422  {csn 3591   class class class wbr 4000  suc csuc 4362  ωcom 4586  (class class class)co 5869   +o coa 6408  cen 6732  Fincfn 6734
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-1o 6411  df-oadd 6415  df-er 6529  df-en 6735  df-fin 6737
This theorem is referenced by:  hashun  10769
  Copyright terms: Public domain W3C validator