Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fin1a2lem13 Structured version   Visualization version   GIF version

Theorem fin1a2lem13 9825
 Description: Lemma for fin1a2 9828. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
Assertion
Ref Expression
fin1a2lem13 (((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) → ¬ (𝐵𝐶) ∈ FinII)

Proof of Theorem fin1a2lem13
Dummy variables 𝑒 𝑓 𝑔 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 488 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → (𝐵𝐶) ∈ FinII)
2 simpll1 1209 . . . 4 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → 𝐴 ⊆ 𝒫 𝐵)
3 ssel2 3910 . . . . . . . . . 10 ((𝐴 ⊆ 𝒫 𝐵𝑔𝐴) → 𝑔 ∈ 𝒫 𝐵)
43elpwid 4508 . . . . . . . . 9 ((𝐴 ⊆ 𝒫 𝐵𝑔𝐴) → 𝑔𝐵)
54ssdifd 4068 . . . . . . . 8 ((𝐴 ⊆ 𝒫 𝐵𝑔𝐴) → (𝑔𝐶) ⊆ (𝐵𝐶))
6 sseq1 3940 . . . . . . . 8 (𝑓 = (𝑔𝐶) → (𝑓 ⊆ (𝐵𝐶) ↔ (𝑔𝐶) ⊆ (𝐵𝐶)))
75, 6syl5ibrcom 250 . . . . . . 7 ((𝐴 ⊆ 𝒫 𝐵𝑔𝐴) → (𝑓 = (𝑔𝐶) → 𝑓 ⊆ (𝐵𝐶)))
87rexlimdva 3243 . . . . . 6 (𝐴 ⊆ 𝒫 𝐵 → (∃𝑔𝐴 𝑓 = (𝑔𝐶) → 𝑓 ⊆ (𝐵𝐶)))
9 eqid 2798 . . . . . . . 8 (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑔𝐴 ↦ (𝑔𝐶))
109elrnmpt 5792 . . . . . . 7 (𝑓 ∈ V → (𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 𝑓 = (𝑔𝐶)))
1110elv 3446 . . . . . 6 (𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 𝑓 = (𝑔𝐶))
12 velpw 4502 . . . . . 6 (𝑓 ∈ 𝒫 (𝐵𝐶) ↔ 𝑓 ⊆ (𝐵𝐶))
138, 11, 123imtr4g 299 . . . . 5 (𝐴 ⊆ 𝒫 𝐵 → (𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) → 𝑓 ∈ 𝒫 (𝐵𝐶)))
1413ssrdv 3921 . . . 4 (𝐴 ⊆ 𝒫 𝐵 → ran (𝑔𝐴 ↦ (𝑔𝐶)) ⊆ 𝒫 (𝐵𝐶))
152, 14syl 17 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → ran (𝑔𝐴 ↦ (𝑔𝐶)) ⊆ 𝒫 (𝐵𝐶))
16 simplrr 777 . . . 4 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → 𝐶𝐴)
17 difid 4284 . . . . . . 7 (𝐶𝐶) = ∅
1817eqcomi 2807 . . . . . 6 ∅ = (𝐶𝐶)
19 difeq1 4043 . . . . . . 7 (𝑔 = 𝐶 → (𝑔𝐶) = (𝐶𝐶))
2019rspceeqv 3586 . . . . . 6 ((𝐶𝐴 ∧ ∅ = (𝐶𝐶)) → ∃𝑔𝐴 ∅ = (𝑔𝐶))
2118, 20mpan2 690 . . . . 5 (𝐶𝐴 → ∃𝑔𝐴 ∅ = (𝑔𝐶))
22 0ex 5175 . . . . . 6 ∅ ∈ V
239elrnmpt 5792 . . . . . 6 (∅ ∈ V → (∅ ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 ∅ = (𝑔𝐶)))
2422, 23ax-mp 5 . . . . 5 (∅ ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 ∅ = (𝑔𝐶))
2521, 24sylibr 237 . . . 4 (𝐶𝐴 → ∅ ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)))
26 ne0i 4250 . . . 4 (∅ ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) → ran (𝑔𝐴 ↦ (𝑔𝐶)) ≠ ∅)
2716, 25, 263syl 18 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → ran (𝑔𝐴 ↦ (𝑔𝐶)) ≠ ∅)
28 simpll2 1210 . . . 4 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → [] Or 𝐴)
299elrnmpt 5792 . . . . . . . 8 (𝑥 ∈ V → (𝑥 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 𝑥 = (𝑔𝐶)))
3029elv 3446 . . . . . . 7 (𝑥 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 𝑥 = (𝑔𝐶))
31 difeq1 4043 . . . . . . . . . 10 (𝑔 = 𝑒 → (𝑔𝐶) = (𝑒𝐶))
3231eqeq2d 2809 . . . . . . . . 9 (𝑔 = 𝑒 → (𝑥 = (𝑔𝐶) ↔ 𝑥 = (𝑒𝐶)))
3332cbvrexvw 3397 . . . . . . . 8 (∃𝑔𝐴 𝑥 = (𝑔𝐶) ↔ ∃𝑒𝐴 𝑥 = (𝑒𝐶))
34 sorpssi 7437 . . . . . . . . . . . . . . . 16 (( [] Or 𝐴 ∧ (𝑒𝐴𝑔𝐴)) → (𝑒𝑔𝑔𝑒))
35 ssdif 4067 . . . . . . . . . . . . . . . . 17 (𝑒𝑔 → (𝑒𝐶) ⊆ (𝑔𝐶))
36 ssdif 4067 . . . . . . . . . . . . . . . . 17 (𝑔𝑒 → (𝑔𝐶) ⊆ (𝑒𝐶))
3735, 36orim12i 906 . . . . . . . . . . . . . . . 16 ((𝑒𝑔𝑔𝑒) → ((𝑒𝐶) ⊆ (𝑔𝐶) ∨ (𝑔𝐶) ⊆ (𝑒𝐶)))
3834, 37syl 17 . . . . . . . . . . . . . . 15 (( [] Or 𝐴 ∧ (𝑒𝐴𝑔𝐴)) → ((𝑒𝐶) ⊆ (𝑔𝐶) ∨ (𝑔𝐶) ⊆ (𝑒𝐶)))
39 sseq2 3941 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑔𝐶) → ((𝑒𝐶) ⊆ 𝑓 ↔ (𝑒𝐶) ⊆ (𝑔𝐶)))
40 sseq1 3940 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑔𝐶) → (𝑓 ⊆ (𝑒𝐶) ↔ (𝑔𝐶) ⊆ (𝑒𝐶)))
4139, 40orbi12d 916 . . . . . . . . . . . . . . 15 (𝑓 = (𝑔𝐶) → (((𝑒𝐶) ⊆ 𝑓𝑓 ⊆ (𝑒𝐶)) ↔ ((𝑒𝐶) ⊆ (𝑔𝐶) ∨ (𝑔𝐶) ⊆ (𝑒𝐶))))
4238, 41syl5ibrcom 250 . . . . . . . . . . . . . 14 (( [] Or 𝐴 ∧ (𝑒𝐴𝑔𝐴)) → (𝑓 = (𝑔𝐶) → ((𝑒𝐶) ⊆ 𝑓𝑓 ⊆ (𝑒𝐶))))
4342expr 460 . . . . . . . . . . . . 13 (( [] Or 𝐴𝑒𝐴) → (𝑔𝐴 → (𝑓 = (𝑔𝐶) → ((𝑒𝐶) ⊆ 𝑓𝑓 ⊆ (𝑒𝐶)))))
4443rexlimdv 3242 . . . . . . . . . . . 12 (( [] Or 𝐴𝑒𝐴) → (∃𝑔𝐴 𝑓 = (𝑔𝐶) → ((𝑒𝐶) ⊆ 𝑓𝑓 ⊆ (𝑒𝐶))))
4511, 44syl5bi 245 . . . . . . . . . . 11 (( [] Or 𝐴𝑒𝐴) → (𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) → ((𝑒𝐶) ⊆ 𝑓𝑓 ⊆ (𝑒𝐶))))
4645ralrimiv 3148 . . . . . . . . . 10 (( [] Or 𝐴𝑒𝐴) → ∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))((𝑒𝐶) ⊆ 𝑓𝑓 ⊆ (𝑒𝐶)))
47 sseq1 3940 . . . . . . . . . . . 12 (𝑥 = (𝑒𝐶) → (𝑥𝑓 ↔ (𝑒𝐶) ⊆ 𝑓))
48 sseq2 3941 . . . . . . . . . . . 12 (𝑥 = (𝑒𝐶) → (𝑓𝑥𝑓 ⊆ (𝑒𝐶)))
4947, 48orbi12d 916 . . . . . . . . . . 11 (𝑥 = (𝑒𝐶) → ((𝑥𝑓𝑓𝑥) ↔ ((𝑒𝐶) ⊆ 𝑓𝑓 ⊆ (𝑒𝐶))))
5049ralbidv 3162 . . . . . . . . . 10 (𝑥 = (𝑒𝐶) → (∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))(𝑥𝑓𝑓𝑥) ↔ ∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))((𝑒𝐶) ⊆ 𝑓𝑓 ⊆ (𝑒𝐶))))
5146, 50syl5ibrcom 250 . . . . . . . . 9 (( [] Or 𝐴𝑒𝐴) → (𝑥 = (𝑒𝐶) → ∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))(𝑥𝑓𝑓𝑥)))
5251rexlimdva 3243 . . . . . . . 8 ( [] Or 𝐴 → (∃𝑒𝐴 𝑥 = (𝑒𝐶) → ∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))(𝑥𝑓𝑓𝑥)))
5333, 52syl5bi 245 . . . . . . 7 ( [] Or 𝐴 → (∃𝑔𝐴 𝑥 = (𝑔𝐶) → ∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))(𝑥𝑓𝑓𝑥)))
5430, 53syl5bi 245 . . . . . 6 ( [] Or 𝐴 → (𝑥 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) → ∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))(𝑥𝑓𝑓𝑥)))
5554ralrimiv 3148 . . . . 5 ( [] Or 𝐴 → ∀𝑥 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))(𝑥𝑓𝑓𝑥))
56 sorpss 7436 . . . . 5 ( [] Or ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∀𝑥 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))∀𝑓 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))(𝑥𝑓𝑓𝑥))
5755, 56sylibr 237 . . . 4 ( [] Or 𝐴 → [] Or ran (𝑔𝐴 ↦ (𝑔𝐶)))
5828, 57syl 17 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → [] Or ran (𝑔𝐴 ↦ (𝑔𝐶)))
59 fin2i 9708 . . 3 ((((𝐵𝐶) ∈ FinII ∧ ran (𝑔𝐴 ↦ (𝑔𝐶)) ⊆ 𝒫 (𝐵𝐶)) ∧ (ran (𝑔𝐴 ↦ (𝑔𝐶)) ≠ ∅ ∧ [] Or ran (𝑔𝐴 ↦ (𝑔𝐶)))) → ran (𝑔𝐴 ↦ (𝑔𝐶)) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)))
601, 15, 27, 58, 59syl22anc 837 . 2 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → ran (𝑔𝐴 ↦ (𝑔𝐶)) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)))
61 simpll3 1211 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → ¬ 𝐴𝐴)
62 difeq1 4043 . . . . . . 7 (𝑔 = 𝑓 → (𝑔𝐶) = (𝑓𝐶))
6362cbvmptv 5133 . . . . . 6 (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐴 ↦ (𝑓𝐶))
6463elrnmpt 5792 . . . . 5 ( ran (𝑔𝐴 ↦ (𝑔𝐶)) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) → ( ran (𝑔𝐴 ↦ (𝑔𝐶)) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)))
6564ibi 270 . . . 4 ( ran (𝑔𝐴 ↦ (𝑔𝐶)) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) → ∃𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))
66 eqid 2798 . . . . . . . . . . . . . . . 16 (𝐶) = (𝐶)
67 difeq1 4043 . . . . . . . . . . . . . . . . 17 (𝑔 = → (𝑔𝐶) = (𝐶))
6867rspceeqv 3586 . . . . . . . . . . . . . . . 16 ((𝐴 ∧ (𝐶) = (𝐶)) → ∃𝑔𝐴 (𝐶) = (𝑔𝐶))
6966, 68mpan2 690 . . . . . . . . . . . . . . 15 (𝐴 → ∃𝑔𝐴 (𝐶) = (𝑔𝐶))
7069adantl 485 . . . . . . . . . . . . . 14 (((𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝐴) → ∃𝑔𝐴 (𝐶) = (𝑔𝐶))
71 vex 3444 . . . . . . . . . . . . . . 15 ∈ V
72 difexg 5195 . . . . . . . . . . . . . . 15 ( ∈ V → (𝐶) ∈ V)
739elrnmpt 5792 . . . . . . . . . . . . . . 15 ((𝐶) ∈ V → ((𝐶) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 (𝐶) = (𝑔𝐶)))
7471, 72, 73mp2b 10 . . . . . . . . . . . . . 14 ((𝐶) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 (𝐶) = (𝑔𝐶))
7570, 74sylibr 237 . . . . . . . . . . . . 13 (((𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝐴) → (𝐶) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)))
76 elssuni 4830 . . . . . . . . . . . . 13 ((𝐶) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) → (𝐶) ⊆ ran (𝑔𝐴 ↦ (𝑔𝐶)))
7775, 76syl 17 . . . . . . . . . . . 12 (((𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝐴) → (𝐶) ⊆ ran (𝑔𝐴 ↦ (𝑔𝐶)))
78 simplr 768 . . . . . . . . . . . 12 (((𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝐴) → ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))
7977, 78sseqtrd 3955 . . . . . . . . . . 11 (((𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝐴) → (𝐶) ⊆ (𝑓𝐶))
8079adantll 713 . . . . . . . . . 10 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → (𝐶) ⊆ (𝑓𝐶))
81 unss2 4108 . . . . . . . . . . 11 ((𝐶) ⊆ (𝑓𝐶) → (𝐶 ∪ (𝐶)) ⊆ (𝐶 ∪ (𝑓𝐶)))
82 uncom 4080 . . . . . . . . . . . . . . 15 (𝐶 ∪ (𝐶)) = ((𝐶) ∪ 𝐶)
83 undif1 4382 . . . . . . . . . . . . . . 15 ((𝐶) ∪ 𝐶) = (𝐶)
8482, 83eqtri 2821 . . . . . . . . . . . . . 14 (𝐶 ∪ (𝐶)) = (𝐶)
8584a1i 11 . . . . . . . . . . . . 13 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → (𝐶 ∪ (𝐶)) = (𝐶))
8661ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → ¬ 𝐴𝐴)
8716ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → 𝐶𝐴)
88 simplrr 777 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))
89 eqeq1 2802 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = (𝑥𝐶) → (𝑒 = ∅ ↔ (𝑥𝐶) = ∅))
90 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) ∧ 𝑥𝐴) → ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))
91 ssdif0 4277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓𝐶 ↔ (𝑓𝐶) = ∅)
9291biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝐶 → (𝑓𝐶) = ∅)
9392ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) ∧ 𝑥𝐴) → (𝑓𝐶) = ∅)
9490, 93eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) ∧ 𝑥𝐴) → ran (𝑔𝐴 ↦ (𝑔𝐶)) = ∅)
95 uni0c 4827 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ran (𝑔𝐴 ↦ (𝑔𝐶)) = ∅ ↔ ∀𝑒 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))𝑒 = ∅)
9694, 95sylib 221 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) ∧ 𝑥𝐴) → ∀𝑒 ∈ ran (𝑔𝐴 ↦ (𝑔𝐶))𝑒 = ∅)
97 eqid 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝐶) = (𝑥𝐶)
98 difeq1 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔 = 𝑥 → (𝑔𝐶) = (𝑥𝐶))
9998rspceeqv 3586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐴 ∧ (𝑥𝐶) = (𝑥𝐶)) → ∃𝑔𝐴 (𝑥𝐶) = (𝑔𝐶))
10097, 99mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐴 → ∃𝑔𝐴 (𝑥𝐶) = (𝑔𝐶))
101 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ∈ V
102 difexg 5195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ V → (𝑥𝐶) ∈ V)
1039elrnmpt 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐶) ∈ V → ((𝑥𝐶) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 (𝑥𝐶) = (𝑔𝐶)))
104101, 102, 103mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥𝐶) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) ↔ ∃𝑔𝐴 (𝑥𝐶) = (𝑔𝐶))
105100, 104sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐴 → (𝑥𝐶) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)))
106105adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) ∧ 𝑥𝐴) → (𝑥𝐶) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)))
10789, 96, 106rspcdva 3573 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) ∧ 𝑥𝐴) → (𝑥𝐶) = ∅)
108 ssdif0 4277 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐶 ↔ (𝑥𝐶) = ∅)
109107, 108sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) ∧ 𝑥𝐴) → 𝑥𝐶)
110109ralrimiva 3149 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) → ∀𝑥𝐴 𝑥𝐶)
111 unissb 4832 . . . . . . . . . . . . . . . . . . . . 21 ( 𝐴𝐶 ↔ ∀𝑥𝐴 𝑥𝐶)
112110, 111sylibr 237 . . . . . . . . . . . . . . . . . . . 20 (((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) → 𝐴𝐶)
113 elssuni 4830 . . . . . . . . . . . . . . . . . . . . 21 (𝐶𝐴𝐶 𝐴)
114113ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) → 𝐶 𝐴)
115112, 114eqssd 3932 . . . . . . . . . . . . . . . . . . 19 (((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) → 𝐴 = 𝐶)
116 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) → 𝐶𝐴)
117115, 116eqeltrd 2890 . . . . . . . . . . . . . . . . . 18 (((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) ∧ 𝑓𝐶) → 𝐴𝐴)
118117ex 416 . . . . . . . . . . . . . . . . 17 ((𝐶𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶)) → (𝑓𝐶 𝐴𝐴))
11987, 88, 118syl2anc 587 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → (𝑓𝐶 𝐴𝐴))
12086, 119mtod 201 . . . . . . . . . . . . . . 15 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → ¬ 𝑓𝐶)
12128ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → [] Or 𝐴)
122 simplrl 776 . . . . . . . . . . . . . . . 16 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → 𝑓𝐴)
123 sorpssi 7437 . . . . . . . . . . . . . . . 16 (( [] Or 𝐴 ∧ (𝑓𝐴𝐶𝐴)) → (𝑓𝐶𝐶𝑓))
124121, 122, 87, 123syl12anc 835 . . . . . . . . . . . . . . 15 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → (𝑓𝐶𝐶𝑓))
125 orel1 886 . . . . . . . . . . . . . . 15 𝑓𝐶 → ((𝑓𝐶𝐶𝑓) → 𝐶𝑓))
126120, 124, 125sylc 65 . . . . . . . . . . . . . 14 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → 𝐶𝑓)
127 undif 4388 . . . . . . . . . . . . . 14 (𝐶𝑓 ↔ (𝐶 ∪ (𝑓𝐶)) = 𝑓)
128126, 127sylib 221 . . . . . . . . . . . . 13 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → (𝐶 ∪ (𝑓𝐶)) = 𝑓)
12985, 128sseq12d 3948 . . . . . . . . . . . 12 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → ((𝐶 ∪ (𝐶)) ⊆ (𝐶 ∪ (𝑓𝐶)) ↔ (𝐶) ⊆ 𝑓))
130 ssun1 4099 . . . . . . . . . . . . 13 ⊆ (𝐶)
131 sstr 3923 . . . . . . . . . . . . 13 (( ⊆ (𝐶) ∧ (𝐶) ⊆ 𝑓) → 𝑓)
132130, 131mpan 689 . . . . . . . . . . . 12 ((𝐶) ⊆ 𝑓𝑓)
133129, 132syl6bi 256 . . . . . . . . . . 11 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → ((𝐶 ∪ (𝐶)) ⊆ (𝐶 ∪ (𝑓𝐶)) → 𝑓))
13481, 133syl5 34 . . . . . . . . . 10 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → ((𝐶) ⊆ (𝑓𝐶) → 𝑓))
13580, 134mpd 15 . . . . . . . . 9 ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) ∧ 𝐴) → 𝑓)
136135ralrimiva 3149 . . . . . . . 8 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) → ∀𝐴 𝑓)
137 unissb 4832 . . . . . . . 8 ( 𝐴𝑓 ↔ ∀𝐴 𝑓)
138136, 137sylibr 237 . . . . . . 7 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) → 𝐴𝑓)
139 elssuni 4830 . . . . . . . 8 (𝑓𝐴𝑓 𝐴)
140139ad2antrl 727 . . . . . . 7 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) → 𝑓 𝐴)
141138, 140eqssd 3932 . . . . . 6 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) → 𝐴 = 𝑓)
142 simprl 770 . . . . . 6 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) → 𝑓𝐴)
143141, 142eqeltrd 2890 . . . . 5 (((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) ∧ (𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶))) → 𝐴𝐴)
144143rexlimdvaa 3244 . . . 4 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → (∃𝑓𝐴 ran (𝑔𝐴 ↦ (𝑔𝐶)) = (𝑓𝐶) → 𝐴𝐴))
14565, 144syl5 34 . . 3 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → ( ran (𝑔𝐴 ↦ (𝑔𝐶)) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)) → 𝐴𝐴))
14661, 145mtod 201 . 2 ((((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) ∧ (𝐵𝐶) ∈ FinII) → ¬ ran (𝑔𝐴 ↦ (𝑔𝐶)) ∈ ran (𝑔𝐴 ↦ (𝑔𝐶)))
14760, 146pm2.65da 816 1 (((𝐴 ⊆ 𝒫 𝐵 ∧ [] Or 𝐴 ∧ ¬ 𝐴𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶𝐴)) → ¬ (𝐵𝐶) ∈ FinII)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  ∪ cuni 4800   ↦ cmpt 5110   Or wor 5437  ran crn 5520   [⊊] crpss 7430  Fincfn 8494  FinIIcfin2 9692 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-dm 5529  df-rn 5530  df-rpss 7431  df-fin2 9699 This theorem is referenced by:  fin1a2s  9827
 Copyright terms: Public domain W3C validator