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

Theorem ac6sfi 6876
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 2665 . . . 4 (𝑢 = ∅ → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑))
2 feq2 5331 . . . . . 6 (𝑢 = ∅ → (𝑓:𝑢𝐵𝑓:∅⟶𝐵))
3 raleq 2665 . . . . . 6 (𝑢 = ∅ → (∀𝑥𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓))
42, 3anbi12d 470 . . . . 5 (𝑢 = ∅ → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
54exbidv 1818 . . . 4 (𝑢 = ∅ → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))
61, 5imbi12d 233 . . 3 (𝑢 = ∅ → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))))
7 raleq 2665 . . . 4 (𝑢 = 𝑤 → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥𝑤𝑦𝐵 𝜑))
8 feq2 5331 . . . . . 6 (𝑢 = 𝑤 → (𝑓:𝑢𝐵𝑓:𝑤𝐵))
9 raleq 2665 . . . . . 6 (𝑢 = 𝑤 → (∀𝑥𝑢 𝜓 ↔ ∀𝑥𝑤 𝜓))
108, 9anbi12d 470 . . . . 5 (𝑢 = 𝑤 → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
1110exbidv 1818 . . . 4 (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
127, 11imbi12d 233 . . 3 (𝑢 = 𝑤 → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓))))
13 raleq 2665 . . . 4 (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑))
14 feq2 5331 . . . . . . 7 (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢𝐵𝑓:(𝑤 ∪ {𝑧})⟶𝐵))
15 raleq 2665 . . . . . . 7 (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))
1614, 15anbi12d 470 . . . . . 6 (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
1716exbidv 1818 . . . . 5 (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)))
18 feq1 5330 . . . . . . 7 (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵𝑔:(𝑤 ∪ {𝑧})⟶𝐵))
19 vex 2733 . . . . . . . . . . 11 𝑓 ∈ V
20 vex 2733 . . . . . . . . . . 11 𝑥 ∈ V
2119, 20fvex 5516 . . . . . . . . . 10 (𝑓𝑥) ∈ V
22 ac6sfi.1 . . . . . . . . . 10 (𝑦 = (𝑓𝑥) → (𝜑𝜓))
2321, 22sbcie 2989 . . . . . . . . 9 ([(𝑓𝑥) / 𝑦]𝜑𝜓)
24 fveq1 5495 . . . . . . . . . 10 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
2524sbceq1d 2960 . . . . . . . . 9 (𝑓 = 𝑔 → ([(𝑓𝑥) / 𝑦]𝜑[(𝑔𝑥) / 𝑦]𝜑))
2623, 25bitr3id 193 . . . . . . . 8 (𝑓 = 𝑔 → (𝜓[(𝑔𝑥) / 𝑦]𝜑))
2726ralbidv 2470 . . . . . . 7 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
2818, 27anbi12d 470 . . . . . 6 (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
2928cbvexv 1911 . . . . 5 (∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
3017, 29bitrdi 195 . . . 4 (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
3113, 30imbi12d 233 . . 3 (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
32 raleq 2665 . . . 4 (𝑢 = 𝐴 → (∀𝑥𝑢𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜑))
33 feq2 5331 . . . . . 6 (𝑢 = 𝐴 → (𝑓:𝑢𝐵𝑓:𝐴𝐵))
34 raleq 2665 . . . . . 6 (𝑢 = 𝐴 → (∀𝑥𝑢 𝜓 ↔ ∀𝑥𝐴 𝜓))
3533, 34anbi12d 470 . . . . 5 (𝑢 = 𝐴 → ((𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ (𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
3635exbidv 1818 . . . 4 (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
3732, 36imbi12d 233 . . 3 (𝑢 = 𝐴 → ((∀𝑥𝑢𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑢𝐵 ∧ ∀𝑥𝑢 𝜓)) ↔ (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))))
38 f0 5388 . . . 4 ∅:∅⟶𝐵
39 0ex 4116 . . . . 5 ∅ ∈ V
40 ral0 3516 . . . . . . 7 𝑥 ∈ ∅ 𝜓
4140biantru 300 . . . . . 6 (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
42 feq1 5330 . . . . . 6 (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔ ∅:∅⟶𝐵))
4341, 42bitr3id 193 . . . . 5 (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵))
4439, 43spcev 2825 . . . 4 (∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
4538, 44mp1i 10 . . 3 (∀𝑥 ∈ ∅ ∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))
46 ssun1 3290 . . . . . . 7 𝑤 ⊆ (𝑤 ∪ {𝑧})
47 ssralv 3211 . . . . . . 7 (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥𝑤𝑦𝐵 𝜑))
4846, 47ax-mp 5 . . . . . 6 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥𝑤𝑦𝐵 𝜑)
4948imim1i 60 . . . . 5 ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)))
50 ssun2 3291 . . . . . . . . 9 {𝑧} ⊆ (𝑤 ∪ {𝑧})
51 ssralv 3211 . . . . . . . . 9 ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑))
5250, 51ax-mp 5 . . . . . . . 8 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑)
53 vex 2733 . . . . . . . . . 10 𝑧 ∈ V
54 ralsnsg 3620 . . . . . . . . . 10 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑[𝑧 / 𝑥]𝑦𝐵 𝜑))
5553, 54ax-mp 5 . . . . . . . . 9 (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑[𝑧 / 𝑥]𝑦𝐵 𝜑)
56 sbcrex 3034 . . . . . . . . 9 ([𝑧 / 𝑥]𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
5755, 56bitri 183 . . . . . . . 8 (∀𝑥 ∈ {𝑧}∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
5852, 57sylib 121 . . . . . . 7 (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑦𝐵 [𝑧 / 𝑥]𝜑)
59 nfv 1521 . . . . . . . 8 𝑦 ¬ 𝑧𝑤
60 nfv 1521 . . . . . . . . 9 𝑦𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)
61 nfv 1521 . . . . . . . . . . 11 𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵
62 nfcv 2312 . . . . . . . . . . . 12 𝑦(𝑤 ∪ {𝑧})
63 nfsbc1v 2973 . . . . . . . . . . . 12 𝑦[(𝑔𝑥) / 𝑦]𝜑
6462, 63nfralxy 2508 . . . . . . . . . . 11 𝑦𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑
6561, 64nfan 1558 . . . . . . . . . 10 𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)
6665nfex 1630 . . . . . . . . 9 𝑦𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)
6760, 66nfim 1565 . . . . . . . 8 𝑦(∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
68 simprl 526 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑓:𝑤𝐵)
69 vex 2733 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
7053, 69f1osn 5482 . . . . . . . . . . . . . . 15 {⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦}
71 f1of 5442 . . . . . . . . . . . . . . 15 ({⟨𝑧, 𝑦⟩}:{𝑧}–1-1-onto→{𝑦} → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
7270, 71mp1i 10 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶{𝑦})
73 simpl2 996 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑦𝐵)
7473snssd 3725 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {𝑦} ⊆ 𝐵)
7572, 74fssd 5360 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵)
76 simpl1 995 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ¬ 𝑧𝑤)
77 disjsn 3645 . . . . . . . . . . . . . 14 ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑤)
7876, 77sylibr 133 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅)
79 fun2 5371 . . . . . . . . . . . . 13 (((𝑓:𝑤𝐵 ∧ {⟨𝑧, 𝑦⟩}:{𝑧}⟶𝐵) ∧ (𝑤 ∩ {𝑧}) = ∅) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
8068, 75, 78, 79syl21anc 1232 . . . . . . . . . . . 12 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵)
81 simprr 527 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥𝑤 𝜓)
82 eleq1a 2242 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑤 → (𝑧 = 𝑥𝑧𝑤))
8382necon3bd 2383 . . . . . . . . . . . . . . . . . 18 (𝑥𝑤 → (¬ 𝑧𝑤𝑧𝑥))
8483impcom 124 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝑤𝑥𝑤) → 𝑧𝑥)
85 fvunsng 5690 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ V ∧ 𝑧𝑥) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥))
8620, 85mpan 422 . . . . . . . . . . . . . . . . 17 (𝑧𝑥 → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥))
87 dfsbcq 2957 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥) → ([((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑[(𝑓𝑥) / 𝑦]𝜑))
8887, 23bitr2di 196 . . . . . . . . . . . . . . . . 17 (((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = (𝑓𝑥) → (𝜓[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
8984, 86, 883syl 17 . . . . . . . . . . . . . . . 16 ((¬ 𝑧𝑤𝑥𝑤) → (𝜓[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9089ralbidva 2466 . . . . . . . . . . . . . . 15 𝑧𝑤 → (∀𝑥𝑤 𝜓 ↔ ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9176, 90syl 14 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥𝑤 𝜓 ↔ ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
9281, 91mpbid 146 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
93 simpl3 997 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → [𝑧 / 𝑥]𝜑)
94 ffun 5350 . . . . . . . . . . . . . . . . 17 ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}))
95 ssun2 3291 . . . . . . . . . . . . . . . . . 18 {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩})
96 vsnid 3615 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ {𝑧}
9769dmsnop 5084 . . . . . . . . . . . . . . . . . . 19 dom {⟨𝑧, 𝑦⟩} = {𝑧}
9896, 97eleqtrri 2246 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}
99 funssfv 5522 . . . . . . . . . . . . . . . . . 18 ((Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ {⟨𝑧, 𝑦⟩} ⊆ (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∧ 𝑧 ∈ dom {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10095, 98, 99mp3an23 1324 . . . . . . . . . . . . . . . . 17 (Fun (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10180, 94, 1003syl 17 . . . . . . . . . . . . . . . 16 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) = ({⟨𝑧, 𝑦⟩}‘𝑧))
10253, 69fvsn 5691 . . . . . . . . . . . . . . . 16 ({⟨𝑧, 𝑦⟩}‘𝑧) = 𝑦
103101, 102eqtr2di 2220 . . . . . . . . . . . . . . 15 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
104 ralsnsg 3620 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑[𝑧 / 𝑥]𝜑))
10553, 104ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑥 ∈ {𝑧}𝜑[𝑧 / 𝑥]𝜑)
106 elsni 3601 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑧} → 𝑥 = 𝑧)
107106fveq2d 5500 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑧} → ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧))
108107eqeq2d 2182 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧)))
109108biimparc 297 . . . . . . . . . . . . . . . . . 18 ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
110 sbceq1a 2964 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) → (𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
111109, 110syl 14 . . . . . . . . . . . . . . . . 17 ((𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
112111ralbidva 2466 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
113105, 112bitr3id 193 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
114103, 113syl 14 . . . . . . . . . . . . . 14 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
11593, 114mpbid 146 . . . . . . . . . . . . 13 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
116 ralun 3309 . . . . . . . . . . . . 13 ((∀𝑥𝑤 [((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
11792, 115, 116syl2anc 409 . . . . . . . . . . . 12 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)
11853, 69opex 4214 . . . . . . . . . . . . . . 15 𝑧, 𝑦⟩ ∈ V
119118snex 4171 . . . . . . . . . . . . . 14 {⟨𝑧, 𝑦⟩} ∈ V
12019, 119unex 4426 . . . . . . . . . . . . 13 (𝑓 ∪ {⟨𝑧, 𝑦⟩}) ∈ V
121 feq1 5330 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵))
122 fveq1 5495 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (𝑔𝑥) = ((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥))
123122sbceq1d 2960 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ([(𝑔𝑥) / 𝑦]𝜑[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
124123ralbidv 2470 . . . . . . . . . . . . . 14 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑))
125121, 124anbi12d 470 . . . . . . . . . . . . 13 (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑦⟩}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑)))
126120, 125spcev 2825 . . . . . . . . . . . 12 (((𝑓 ∪ {⟨𝑧, 𝑦⟩}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {⟨𝑧, 𝑦⟩})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
12780, 117, 126syl2anc 409 . . . . . . . . . . 11 (((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))
128127ex 114 . . . . . . . . . 10 ((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) → ((𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
129128exlimdv 1812 . . . . . . . . 9 ((¬ 𝑧𝑤𝑦𝐵[𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))
1301293exp 1197 . . . . . . . 8 𝑧𝑤 → (𝑦𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑)))))
13159, 67, 130rexlimd 2584 . . . . . . 7 𝑧𝑤 → (∃𝑦𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
13258, 131syl5 32 . . . . . 6 𝑧𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → (∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
133132a2d 26 . . . . 5 𝑧𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
13449, 133syl5 32 . . . 4 𝑧𝑤 → ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
135134adantl 275 . . 3 ((𝑤 ∈ Fin ∧ ¬ 𝑧𝑤) → ((∀𝑥𝑤𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝑤𝐵 ∧ ∀𝑥𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔𝑥) / 𝑦]𝜑))))
1366, 12, 31, 37, 45, 135findcard2s 6868 . 2 (𝐴 ∈ Fin → (∀𝑥𝐴𝑦𝐵 𝜑 → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓)))
137136imp 123 1 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  w3a 973   = wceq 1348  wex 1485  wcel 2141  wne 2340  wral 2448  wrex 2449  Vcvv 2730  [wsbc 2955  cun 3119  cin 3120  wss 3121  c0 3414  {csn 3583  cop 3586  dom cdm 4611  Fun wfun 5192  wf 5194  1-1-ontowf1o 5197  cfv 5198  Fincfn 6718
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-er 6513  df-en 6719  df-fin 6721
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator