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

Theorem ac6sfi 6843
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 2652 . . . 4 (𝑢 = ∅ → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑))
2 feq2 5303 . . . . . 6 (𝑢 = ∅ → (𝑓:𝑢𝐵𝑓:∅⟶𝐵))
3 raleq 2652 . . . . . 6 (𝑢 = ∅ → (∀𝑥𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓))
42, 3anbi12d 465 . . . . 5 (𝑢 = ∅ → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
54exbidv 1805 . . . 4 (𝑢 = ∅ → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
61, 5imbi12d 233 . . 3 (𝑢 = ∅ → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))))
7 raleq 2652 . . . 4 (𝑢 = 𝑤 → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥𝑤𝑦𝐵 𝜑))
8 feq2 5303 . . . . . 6 (𝑢 = 𝑤 → (𝑓:𝑢𝐵𝑓:𝑤𝐵))
9 raleq 2652 . . . . . 6 (𝑢 = 𝑤 → (∀𝑥𝑢 𝜓 ↔ ∀𝑥𝑤 𝜓))
108, 9anbi12d 465 . . . . 5 (𝑢 = 𝑤 → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
1110exbidv 1805 . . . 4 (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
127, 11imbi12d 233 . . 3 (𝑢 = 𝑤 → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓))))
13 raleq 2652 . . . 4 (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑))
14 feq2 5303 . . . . . . 7 (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢𝐵𝑓:(𝑤 ∪ {𝑧})⟶𝐵))
15 raleq 2652 . . . . . . 7 (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))
1614, 15anbi12d 465 . . . . . 6 (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
1716exbidv 1805 . . . . 5 (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
18 feq1 5302 . . . . . . 7 (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵𝑔:(𝑤 ∪ {𝑧})⟶𝐵))
19 vex 2715 . . . . . . . . . . 11 𝑓 ∈ V
20 vex 2715 . . . . . . . . . . 11 𝑥 ∈ V
2119, 20fvex 5488 . . . . . . . . . 10 (𝑓𝑥) ∈ V
22 ac6sfi.1 . . . . . . . . . 10 (𝑦 = (𝑓𝑥) → (𝜑𝜓))
2321, 22sbcie 2971 . . . . . . . . 9 ([(𝑓𝑥) / 𝑦]𝜑𝜓)
24 fveq1 5467 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
2524sbceq1d 2942 . . . . . . . . 9 (𝑓 = 𝑔 → ([(𝑓𝑥) / 𝑦]𝜑[(𝑔𝑥) / 𝑦]𝜑))
2623, 25bitr3id 193 . . . . . . . 8 (𝑓 = 𝑔 → (𝜓[(𝑔𝑥) / 𝑦]𝜑))
2726ralbidv 2457 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
2818, 27anbi12d 465 . . . . . 6 (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
2928cbvexv 1898 . . . . 5 (∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
3017, 29bitrdi 195 . . . 4 (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
3113, 30imbi12d 233 . . 3 (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
32 raleq 2652 . . . 4 (𝑢 = 𝐴 → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜑))
33 feq2 5303 . . . . . 6 (𝑢 = 𝐴 → (𝑓:𝑢𝐵𝑓:𝐴𝐵))
34 raleq 2652 . . . . . 6 (𝑢 = 𝐴 → (∀𝑥𝑢 𝜓 ↔ ∀𝑥𝐴 𝜓))
3533, 34anbi12d 465 . . . . 5 (𝑢 = 𝐴 → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
3635exbidv 1805 . . . 4 (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
3732, 36imbi12d 233 . . 3 (𝑢 = 𝐴 → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))))
38 f0 5360 . . . 4 ∅:∅⟶𝐵
39 0ex 4091 . . . . 5 ∅ ∈ V
40 ral0 3495 . . . . . . 7 𝑥 ∈ ∅ 𝜓
4140biantru 300 . . . . . 6 (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
42 feq1 5302 . . . . . 6 (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔ ∅:∅⟶𝐵))
4341, 42bitr3id 193 . . . . 5 (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵))
4439, 43spcev 2807 . . . 4 (∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
4538, 44mp1i 10 . . 3 (∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
46 ssun1 3270 . . . . . . 7 𝑤 ⊆ (𝑤 ∪ {𝑧})
47 ssralv 3192 . . . . . . 7 (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥𝑤𝑦𝐵 𝜑))
4846, 47ax-mp 5 . . . . . 6 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥𝑤𝑦𝐵 𝜑)
4948imim1i 60 . . . . 5 ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
50 ssun2 3271 . . . . . . . . 9 {𝑧} ⊆ (𝑤 ∪ {𝑧})
51 ssralv 3192 . . . . . . . . 9 ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑))
5250, 51ax-mp 5 . . . . . . . 8 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑)
53 vex 2715 . . . . . . . . . 10 𝑧 ∈ V
54 ralsnsg 3596 . . . . . . . . . 10 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑[𝑧 / 𝑥]𝑦𝐵 𝜑))
5553, 54ax-mp 5 . . . . . . . . 9 (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑[𝑧 / 𝑥]𝑦𝐵 𝜑)
56 sbcrex 3016 . . . . . . . . 9 ([𝑧 / 𝑥]𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
5755, 56bitri 183 . . . . . . . 8 (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
5852, 57sylib 121 . . . . . . 7 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
59 nfv 1508 . . . . . . . 8 𝑦 ¬ 𝑧𝑤
60 nfv 1508 . . . . . . . . 9 𝑦𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)
61 nfv 1508 . . . . . . . . . . 11 𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵
62 nfcv 2299 . . . . . . . . . . . 12 𝑦(𝑤 ∪ {𝑧})
63 nfsbc1v 2955 . . . . . . . . . . . 12 𝑦[(𝑔𝑥) / 𝑦]𝜑
6462, 63nfralxy 2495 . . . . . . . . . . 11 𝑦𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑
6561, 64nfan 1545 . . . . . . . . . 10 𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)
6665nfex 1617 . . . . . . . . 9 𝑦𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)
6760, 66nfim 1552 . . . . . . . 8 𝑦(∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
68 simprl 521 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑓:𝑤𝐵)
69 vex 2715 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
7053, 69f1osn 5454 . . . . . . . . . . . . . . 15 {⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦}
71 f1of 5414 . . . . . . . . . . . . . . 15 ({⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦} → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
7270, 71mp1i 10 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
73 simpl2 986 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑦𝐵)
7473snssd 3701 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {𝑦} ⊆ 𝐵)
7572, 74fssd 5332 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵)
76 simpl1 985 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ¬ 𝑧𝑤)
77 disjsn 3621 . . . . . . . . . . . . . 14 ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑤)
7876, 77sylibr 133 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅)
79 fun2 5343 . . . . . . . . . . . . 13 (((𝑓:𝑤𝐵 ∧ {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵) ∧ (𝑤 ∩ {𝑧}) = ∅) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
8068, 75, 78, 79syl21anc 1219 . . . . . . . . . . . 12 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
81 simprr 522 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥𝑤 𝜓)
82 eleq1a 2229 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑤 → (𝑧 = 𝑥𝑧𝑤))
8382necon3bd 2370 . . . . . . . . . . . . . . . . . 18 (𝑥𝑤 → (¬ 𝑧𝑤𝑧𝑥))
8483impcom 124 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝑤𝑥𝑤) → 𝑧𝑥)
85 fvunsng 5661 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ V ∧ 𝑧𝑥) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥))
8620, 85mpan 421 . . . . . . . . . . . . . . . . 17 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥))
87 dfsbcq 2939 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥) → ([((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑[(𝑓𝑥) / 𝑦]𝜑))
8887, 23bitr2di 196 . . . . . . . . . . . . . . . . 17 (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥) → (𝜓[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
8984, 86, 883syl 17 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑤𝑥𝑤) → (𝜓[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9089ralbidva 2453 . . . . . . . . . . . . . . 15 𝑧𝑤 → (∀𝑥𝑤 𝜓 ↔ ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9176, 90syl 14 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥𝑤 𝜓 ↔ ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9281, 91mpbid 146 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
93 simpl3 987 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → [𝑧 / 𝑥]𝜑)
94 ffun 5322 . . . . . . . . . . . . . . . . 17 ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}))
95 ssun2 3271 . . . . . . . . . . . . . . . . . 18 {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩})
96 vsnid 3592 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
9769dmsnop 5059 . . . . . . . . . . . . . . . . . . 19 dom {⟨𝑧, 𝑦⟩} = {𝑧}
9896, 97eleqtrri 2233 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}
99 funssfv 5494 . . . . . . . . . . . . . . . . . 18 ((Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10095, 98, 99mp3an23 1311 . . . . . . . . . . . . . . . . 17 (Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10180, 94, 1003syl 17 . . . . . . . . . . . . . . . 16 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10253, 69fvsn 5662 . . . . . . . . . . . . . . . 16 ({⟨𝑧, 𝑦⟩}‘𝑧) = 𝑦
103101, 102eqtr2di 2207 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
104 ralsnsg 3596 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑[𝑧 / 𝑥]𝜑))
10553, 104ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ {𝑧}𝜑[𝑧 / 𝑥]𝜑)
106 elsni 3578 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
107106fveq2d 5472 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑧} → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
108107eqeq2d 2169 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧)))
109108biimparc 297 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
110 sbceq1a 2946 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) → (𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
111109, 110syl 14 . . . . . . . . . . . . . . . . 17 ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
112111ralbidva 2453 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
113105, 112bitr3id 193 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
114103, 113syl 14 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
11593, 114mpbid 146 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
116 ralun 3289 . . . . . . . . . . . . 13 ((∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
11792, 115, 116syl2anc 409 . . . . . . . . . . . 12 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
11853, 69opex 4189 . . . . . . . . . . . . . . 15 𝑧, 𝑦⟩ ∈ V
119118snex 4146 . . . . . . . . . . . . . 14 {⟨𝑧, 𝑦⟩} ∈ V
12019, 119unex 4401 . . . . . . . . . . . . 13 (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∈ V
121 feq1 5302 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵))
122 fveq1 5467 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
123122sbceq1d 2942 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ([(𝑔𝑥) / 𝑦]𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
124123ralbidv 2457 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
125121, 124anbi12d 465 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)))
126120, 125spcev 2807 . . . . . . . . . . . 12 (((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
12780, 117, 126syl2anc 409 . . . . . . . . . . 11 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
128127ex 114 . . . . . . . . . 10 ((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) → ((𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
129128exlimdv 1799 . . . . . . . . 9 ((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
1301293exp 1184 . . . . . . . 8 𝑧𝑤 → (𝑦𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))))
13159, 67, 130rexlimd 2571 . . . . . . 7 𝑧𝑤 → (∃𝑦𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
13258, 131syl5 32 . . . . . 6 𝑧𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
133132a2d 26 . . . . 5 𝑧𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
13449, 133syl5 32 . . . 4 𝑧𝑤 → ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
135134adantl 275 . . 3 ((𝑤 ∈ Fin ∧ ¬ 𝑧𝑤) → ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
1366, 12, 31, 37, 45, 135findcard2s 6835 . 2 (𝐴 ∈ Fin → (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
137136imp 123 1 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  w3a 963   = wceq 1335  wex 1472  wcel 2128  wne 2327  wral 2435  wrex 2436  Vcvv 2712  [wsbc 2937  cun 3100  cin 3101  wss 3102  c0 3394  {csn 3560  cop 3563  dom cdm 4586  Fun wfun 5164  wf 5166  1-1-ontowf1o 5169  cfv 5170  Fincfn 6685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4496  ax-iinf 4547
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4253  df-iord 4326  df-on 4328  df-suc 4331  df-iom 4550  df-xp 4592  df-rel 4593  df-cnv 4594  df-co 4595  df-dm 4596  df-rn 4597  df-res 4598  df-ima 4599  df-iota 5135  df-fun 5172  df-fn 5173  df-f 5174  df-f1 5175  df-fo 5176  df-f1o 5177  df-fv 5178  df-er 6480  df-en 6686  df-fin 6688
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator