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

Theorem ac6sfi 6544
Description: Existence of a choice function for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
Hypothesis
Ref Expression
ac6sfi.1 (𝑦 = (𝑓𝑥) → (𝜑𝜓))
Assertion
Ref Expression
ac6sfi ((𝐴 ∈ Fin ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))
Distinct variable groups:   𝑥,𝑓,𝐴   𝑦,𝑓,𝐵,𝑥   𝜑,𝑓   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑓)   𝐴(𝑦)

Proof of Theorem ac6sfi
Dummy variables 𝑢 𝑤 𝑧 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 2555 . . . 4 (𝑢 = ∅ → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑))
2 feq2 5099 . . . . . 6 (𝑢 = ∅ → (𝑓:𝑢𝐵𝑓:∅⟶𝐵))
3 raleq 2555 . . . . . 6 (𝑢 = ∅ → (∀𝑥𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓))
42, 3anbi12d 457 . . . . 5 (𝑢 = ∅ → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
54exbidv 1748 . . . 4 (𝑢 = ∅ → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
61, 5imbi12d 232 . . 3 (𝑢 = ∅ → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))))
7 raleq 2555 . . . 4 (𝑢 = 𝑤 → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥𝑤𝑦𝐵 𝜑))
8 feq2 5099 . . . . . 6 (𝑢 = 𝑤 → (𝑓:𝑢𝐵𝑓:𝑤𝐵))
9 raleq 2555 . . . . . 6 (𝑢 = 𝑤 → (∀𝑥𝑢 𝜓 ↔ ∀𝑥𝑤 𝜓))
108, 9anbi12d 457 . . . . 5 (𝑢 = 𝑤 → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
1110exbidv 1748 . . . 4 (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
127, 11imbi12d 232 . . 3 (𝑢 = 𝑤 → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓))))
13 raleq 2555 . . . 4 (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑))
14 feq2 5099 . . . . . . 7 (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢𝐵𝑓:(𝑤 ∪ {𝑧})⟶𝐵))
15 raleq 2555 . . . . . . 7 (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))
1614, 15anbi12d 457 . . . . . 6 (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
1716exbidv 1748 . . . . 5 (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
18 feq1 5098 . . . . . . 7 (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵𝑔:(𝑤 ∪ {𝑧})⟶𝐵))
19 vex 2615 . . . . . . . . . . 11 𝑓 ∈ V
20 vex 2615 . . . . . . . . . . 11 𝑥 ∈ V
2119, 20fvex 5270 . . . . . . . . . 10 (𝑓𝑥) ∈ V
22 ac6sfi.1 . . . . . . . . . 10 (𝑦 = (𝑓𝑥) → (𝜑𝜓))
2321, 22sbcie 2859 . . . . . . . . 9 ([(𝑓𝑥) / 𝑦]𝜑𝜓)
24 fveq1 5252 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
2524sbceq1d 2831 . . . . . . . . 9 (𝑓 = 𝑔 → ([(𝑓𝑥) / 𝑦]𝜑[(𝑔𝑥) / 𝑦]𝜑))
2623, 25syl5bbr 192 . . . . . . . 8 (𝑓 = 𝑔 → (𝜓[(𝑔𝑥) / 𝑦]𝜑))
2726ralbidv 2374 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
2818, 27anbi12d 457 . . . . . 6 (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
2928cbvexv 1838 . . . . 5 (∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
3017, 29syl6bb 194 . . . 4 (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
3113, 30imbi12d 232 . . 3 (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
32 raleq 2555 . . . 4 (𝑢 = 𝐴 → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜑))
33 feq2 5099 . . . . . 6 (𝑢 = 𝐴 → (𝑓:𝑢𝐵𝑓:𝐴𝐵))
34 raleq 2555 . . . . . 6 (𝑢 = 𝐴 → (∀𝑥𝑢 𝜓 ↔ ∀𝑥𝐴 𝜓))
3533, 34anbi12d 457 . . . . 5 (𝑢 = 𝐴 → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
3635exbidv 1748 . . . 4 (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
3732, 36imbi12d 232 . . 3 (𝑢 = 𝐴 → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))))
38 f0 5149 . . . 4 ∅:∅⟶𝐵
39 0ex 3931 . . . . 5 ∅ ∈ V
40 ral0 3364 . . . . . . 7 𝑥 ∈ ∅ 𝜓
4140biantru 296 . . . . . 6 (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
42 feq1 5098 . . . . . 6 (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔ ∅:∅⟶𝐵))
4341, 42syl5bbr 192 . . . . 5 (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵))
4439, 43spcev 2703 . . . 4 (∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
4538, 44mp1i 10 . . 3 (∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
46 ssun1 3147 . . . . . . 7 𝑤 ⊆ (𝑤 ∪ {𝑧})
47 ssralv 3069 . . . . . . 7 (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥𝑤𝑦𝐵 𝜑))
4846, 47ax-mp 7 . . . . . 6 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥𝑤𝑦𝐵 𝜑)
4948imim1i 59 . . . . 5 ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
50 ssun2 3148 . . . . . . . . 9 {𝑧} ⊆ (𝑤 ∪ {𝑧})
51 ssralv 3069 . . . . . . . . 9 ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑))
5250, 51ax-mp 7 . . . . . . . 8 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑)
53 vex 2615 . . . . . . . . . 10 𝑧 ∈ V
54 ralsnsg 3454 . . . . . . . . . 10 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑[𝑧 / 𝑥]𝑦𝐵 𝜑))
5553, 54ax-mp 7 . . . . . . . . 9 (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑[𝑧 / 𝑥]𝑦𝐵 𝜑)
56 sbcrex 2904 . . . . . . . . 9 ([𝑧 / 𝑥]𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
5755, 56bitri 182 . . . . . . . 8 (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
5852, 57sylib 120 . . . . . . 7 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
59 nfv 1462 . . . . . . . 8 𝑦 ¬ 𝑧𝑤
60 nfv 1462 . . . . . . . . 9 𝑦𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)
61 nfv 1462 . . . . . . . . . . 11 𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵
62 nfcv 2223 . . . . . . . . . . . 12 𝑦(𝑤 ∪ {𝑧})
63 nfsbc1v 2844 . . . . . . . . . . . 12 𝑦[(𝑔𝑥) / 𝑦]𝜑
6462, 63nfralxy 2408 . . . . . . . . . . 11 𝑦𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑
6561, 64nfan 1498 . . . . . . . . . 10 𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)
6665nfex 1569 . . . . . . . . 9 𝑦𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)
6760, 66nfim 1505 . . . . . . . 8 𝑦(∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
68 simprl 498 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑓:𝑤𝐵)
69 vex 2615 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
7053, 69f1osn 5241 . . . . . . . . . . . . . . 15 {⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦}
71 f1of 5201 . . . . . . . . . . . . . . 15 ({⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦} → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
7270, 71mp1i 10 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
73 simpl2 943 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑦𝐵)
7473snssd 3556 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {𝑦} ⊆ 𝐵)
7572, 74fssd 5124 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵)
76 simpl1 942 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ¬ 𝑧𝑤)
77 disjsn 3478 . . . . . . . . . . . . . 14 ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑤)
7876, 77sylibr 132 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅)
79 fun2 5133 . . . . . . . . . . . . 13 (((𝑓:𝑤𝐵 ∧ {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵) ∧ (𝑤 ∩ {𝑧}) = ∅) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
8068, 75, 78, 79syl21anc 1169 . . . . . . . . . . . 12 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
81 simprr 499 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥𝑤 𝜓)
82 eleq1a 2154 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑤 → (𝑧 = 𝑥𝑧𝑤))
8382necon3bd 2292 . . . . . . . . . . . . . . . . . 18 (𝑥𝑤 → (¬ 𝑧𝑤𝑧𝑥))
8483impcom 123 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝑤𝑥𝑤) → 𝑧𝑥)
85 fvunsng 5433 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ V ∧ 𝑧𝑥) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥))
8620, 85mpan 415 . . . . . . . . . . . . . . . . 17 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥))
87 dfsbcq 2828 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥) → ([((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑[(𝑓𝑥) / 𝑦]𝜑))
8887, 23syl6rbb 195 . . . . . . . . . . . . . . . . 17 (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥) → (𝜓[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
8984, 86, 883syl 17 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑤𝑥𝑤) → (𝜓[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9089ralbidva 2370 . . . . . . . . . . . . . . 15 𝑧𝑤 → (∀𝑥𝑤 𝜓 ↔ ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9176, 90syl 14 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥𝑤 𝜓 ↔ ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9281, 91mpbid 145 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
93 simpl3 944 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → [𝑧 / 𝑥]𝜑)
94 ffun 5117 . . . . . . . . . . . . . . . . 17 ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}))
95 ssun2 3148 . . . . . . . . . . . . . . . . . 18 {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩})
96 vsnid 3450 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
9769dmsnop 4858 . . . . . . . . . . . . . . . . . . 19 dom {⟨𝑧, 𝑦⟩} = {𝑧}
9896, 97eleqtrri 2158 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}
99 funssfv 5275 . . . . . . . . . . . . . . . . . 18 ((Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10095, 98, 99mp3an23 1261 . . . . . . . . . . . . . . . . 17 (Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10180, 94, 1003syl 17 . . . . . . . . . . . . . . . 16 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10253, 69fvsn 5434 . . . . . . . . . . . . . . . 16 ({⟨𝑧, 𝑦⟩}‘𝑧) = 𝑦
103101, 102syl6req 2132 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
104 ralsnsg 3454 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑[𝑧 / 𝑥]𝜑))
10553, 104ax-mp 7 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ {𝑧}𝜑[𝑧 / 𝑥]𝜑)
106 elsni 3440 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
107106fveq2d 5257 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑧} → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
108107eqeq2d 2094 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧)))
109108biimparc 293 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
110 sbceq1a 2835 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) → (𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
111109, 110syl 14 . . . . . . . . . . . . . . . . 17 ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
112111ralbidva 2370 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
113105, 112syl5bbr 192 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
114103, 113syl 14 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
11593, 114mpbid 145 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
116 ralun 3166 . . . . . . . . . . . . 13 ((∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
11792, 115, 116syl2anc 403 . . . . . . . . . . . 12 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
11853, 69opex 4020 . . . . . . . . . . . . . . 15 𝑧, 𝑦⟩ ∈ V
119118snex 3984 . . . . . . . . . . . . . 14 {⟨𝑧, 𝑦⟩} ∈ V
12019, 119unex 4230 . . . . . . . . . . . . 13 (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∈ V
121 feq1 5098 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵))
122 fveq1 5252 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
123122sbceq1d 2831 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ([(𝑔𝑥) / 𝑦]𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
124123ralbidv 2374 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
125121, 124anbi12d 457 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)))
126120, 125spcev 2703 . . . . . . . . . . . 12 (((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
12780, 117, 126syl2anc 403 . . . . . . . . . . 11 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
128127ex 113 . . . . . . . . . 10 ((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) → ((𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
129128exlimdv 1742 . . . . . . . . 9 ((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
1301293exp 1138 . . . . . . . 8 𝑧𝑤 → (𝑦𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))))
13159, 67, 130rexlimd 2480 . . . . . . 7 𝑧𝑤 → (∃𝑦𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
13258, 131syl5 32 . . . . . 6 𝑧𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
133132a2d 26 . . . . 5 𝑧𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
13449, 133syl5 32 . . . 4 𝑧𝑤 → ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
135134adantl 271 . . 3 ((𝑤 ∈ Fin ∧ ¬ 𝑧𝑤) → ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
1366, 12, 31, 37, 45, 135findcard2s 6536 . 2 (𝐴 ∈ Fin → (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
137136imp 122 1 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  w3a 920   = wceq 1285  wex 1422  wcel 1434  wne 2249  wral 2353  wrex 2354  Vcvv 2612  [wsbc 2826  cun 2982  cin 2983  wss 2984  c0 3269  {csn 3422  cop 3425  dom cdm 4401  Fun wfun 4963  wf 4965  1-1-ontowf1o 4968  cfv 4969  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-er 6222  df-en 6388  df-fin 6390
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator